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