Theorem: lebits=>nat-of-nat=>lebits
(defthm lebits=>nat-of-nat=>lebits (implies (< (nfix nat) (expt 2 (nfix width))) (equal (lebits=>nat (nat=>lebits width nat)) (nfix nat))))