proposition: Lemma ideal_rigunel2 {R : rig} (I : ideal R) : I 1 -> forall x, I x.
proof: Proof. intros H x. apply (transportf (λ x, I x) (rigrunax2 _ x)). exact (ideal_isl _ _ _ H). Qed.
imports: UniMath.Algebra.RigsAndRings UniMath.MoreFoundations.Notations