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