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