Relation between signed short and signed int minima.
Theorem: sshort-min-vs-sint-min
(defthm sshort-min-vs-sint-min (> (sshort-min) (sint-min)) :rule-classes :linear)