Theorem Nat.supᵢ_lt_succ

Modification history