Theorem: leubyte11s=>nat-of-nat=>leubyte11s+
(defthm leubyte11s=>nat-of-nat=>leubyte11s+ (equal (leubyte11s=>nat (nat=>leubyte11s+ nat)) (nfix nat)))