Theorem Nat.succPNat_mono

Modification history