Relation between unsigned char and signed int maxima.
Theorem: ushort-max-vs-slong-max
(defthm ushort-max-vs-slong-max (<= (ushort-max) (slong-max)) :rule-classes ((:linear :trigger-terms ((ushort-max) (slong-max)))))