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