Relation between unsigned long and signed long long maxima.
Theorem: ulong-max-vs-sllong-max
(defthm ulong-max-vs-sllong-max (> (ulong-max) (sllong-max)) :rule-classes ((:linear :trigger-terms ((ulong-max) (sllong-max)))))