proposition: Lemma ideal_closed_0 : P 0.
proof: Proof. destruct ideal_NonEmpty as [[x Px]]. rewrite <-(plus_negate_r x). intuition. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.theory.rings MathClasses.theory.ring_congruence