Relation between unsigned long and unsigned long long maxima.
Theorem: ulong-max-vs-ullong-max
(defthm ulong-max-vs-ullong-max (= (ulong-max) (ullong-max)) :rule-classes :linear)