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