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