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