Alternative definition of slong-integerp as integer range.
Theorem: slong-integerp-alt-def
(defthm slong-integerp-alt-def (equal (slong-integerp x) (and (integerp x) (<= (slong-min) x) (<= x (slong-max)))))
