Relation between unsigned char and unsigned short maxima.
Theorem: uchar-max-vs-ushort-max
(defthm uchar-max-vs-ushort-max (< (uchar-max) (ushort-max)) :rule-classes :linear)