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