Theorem: nat=>lebytes-of-lebytes=>nat
(defthm nat=>lebytes-of-lebytes=>nat (equal (nat=>lebytes (len digits) (lebytes=>nat digits)) (byte-list-fix digits)))