Theorem Nat.succPNat_lt_succPNat

Modification history