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