proposition: Lemma isaset_ideal : isaset ideal.
proof: Proof. apply isaset_total2. - apply isaset_submonoid. - intro S. apply isasetaprop, propproperty. Defined.
imports: UniMath.Algebra.RigsAndRings UniMath.MoreFoundations.Notations