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