Theorem: nat=>leubyte11s+-of-leubyte11s=>nat
(defthm nat=>leubyte11s+-of-leubyte11s=>nat (equal (nat=>leubyte11s+ (leubyte11s=>nat digits)) (trim-lendian+ (ubyte11-list-fix digits))))