Theorem Nat.sInf_upward_closed_eq_succ_iff

Modification history