Theorem Nat.succPNat_injective

Modification history