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