Theorem: leubyte11s=>nat-of-nat=>leubyte11s
(defthm leubyte11s=>nat-of-nat=>leubyte11s (implies (< (nfix nat) (expt 2048 (nfix width))) (equal (leubyte11s=>nat (nat=>leubyte11s width nat)) (nfix nat))))