Lemma commrig_ideals (R : commrig) (S : subabmonoid (rigaddabmonoid R)) : is_lideal S ≃ is_rideal S. Proof. apply weqimplimpl. - intros islid r s ss. use transportf. + exact (S (r * s)). + exact (maponpaths S (rigcomm2 _ _ _)). + apply (islid r s ss). - intros isrid r s ss. use transportf. + exact (S (s * r)). + exact (maponpaths S (rigcomm2 _ _ _)). + apply (isrid r s ss). - apply propproperty. - apply propproperty. Defined.
Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.MoreFoundations.Notations.