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