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