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