Theorem Nat.add_eq_max_iff

Modification history