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