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