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