Relation between signed long and signed long long maxima.
Theorem: slong-max-vs-sllong-max
(defthm slong-max-vs-sllong-max (= (slong-max) (sllong-max)) :rule-classes :linear)