Theorem: nat=>lebits+-injectivity
(defthm nat=>lebits+-injectivity (equal (equal (nat=>lebits+ nat1) (nat=>lebits+ nat2)) (equal (nfix nat1) (nfix nat2))))