proposition: Lemma isaset_prime_ideal : isaset (prime_ideal R).
proof: Proof. apply isaset_total2. - apply isaset_ideal. - intro I. apply isasetaprop, propproperty. Qed.
imports: UniMath.Algebra.RigsAndRings UniMath.MoreFoundations.Notations