Theorem: nat=>lebits-injectivity
(defthm nat=>lebits-injectivity (implies (and (< (nfix nat1) (expt 2 (nfix width))) (< (nfix nat2) (expt 2 (nfix width)))) (equal (equal (nat=>lebits width nat1) (nat=>lebits width nat2)) (equal (nfix nat1) (nfix nat2)))))