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