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