Behavior of integer-length on bad inputs.
Theorem: integer-length-default
(defthm integer-length-default (implies (not (integerp x)) (equal (integer-length x) 0)) :rule-classes ((:rewrite :backchain-limit-lst 0)))
