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