Theorem:
(defthm nat=>leubyte11s-injectivity (implies (and (< (nfix nat1) (expt 2048 (nfix width))) (< (nfix nat2) (expt 2048 (nfix width)))) (equal (equal (nat=>leubyte11s width nat1) (nat=>leubyte11s width nat2)) (equal (nfix nat1) (nfix nat2)))))