Theorem: lebytes=>nat-of-nat=>lebytes+
(defthm lebytes=>nat-of-nat=>lebytes+ (equal (lebytes=>nat (nat=>lebytes+ nat)) (nfix nat)))