Definition make_prime_ideal (p : ideal R) (H1 : ∀ a b, p (a * b) ⇒ p a ∨ p b) (H2 : ¬ p 1) : prime_ideal := p ,, H1 ,, H2.
Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.MoreFoundations.Notations.