General relation between unsigned short and unsigned int maxima.
Theorem: ushort-max-<=-uint-max
(defthm ushort-max-<=-uint-max (<= (ushort-max) (uint-max)) :rule-classes :linear)