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