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