Relation between unsigned int and unsigned long maxima.
Theorem: uint-max-vs-ulong-max
(defthm uint-max-vs-ulong-max (< (uint-max) (ulong-max)) :rule-classes :linear)