Definition prime_ideal_complement (p : prime_ideal R) : subabmonoid (ringmultabmonoid R). Proof. use make_submonoid. - intro x. exact (¬ p x). - use make_issubmonoid. + intros a b. exact (prime_ideal_ax1_contraposition _ _ _ (pr2 a) (pr2 b)). + exact (prime_ideal_ax2 p). Defined.
Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.MoreFoundations.Notations.