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