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