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