Theorem Nat.succ_lt_succ_iff

Modification history