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