Relation between int and long bit sizes.
Theorem: int-bits-vs-long-bits
(defthm int-bits-vs-long-bits (< (int-bits) (long-bits)) :rule-classes ((:linear :trigger-terms ((int-bits) (long-bits)))))