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