proposition: Lemma ideal_closed_plus x y : P x → P y → P (x + y).
proof: Proof. intros. assert (x + y = -(-x + -y)) as E by ring. rewrite E. intuition. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.theory.rings MathClasses.theory.ring_congruence