Relation between unsigned int and signed long long maxima.
Theorem: uchar-max-vs-sllong-max
(defthm uchar-max-vs-sllong-max (<= (uchar-max) (sllong-max)) :rule-classes ((:linear :trigger-terms ((uchar-max) (sllong-max)))))