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