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