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