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