Theorem Nat.succPNat_inj

Modification history