Relation between signed char and signed short maxima.
Theorem: schar-max-vs-sshort-max
(defthm schar-max-vs-sshort-max (< (schar-max) (sshort-max)) :rule-classes :linear)