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