Lemma rigtoringlunit2 (X : rig) : islunit (rigtoringop2 X) (rigtoringunel2 X). Proof. unfold islunit. apply (setquotunivprop _ (λ x, _ = _)). intro x. change (setquotpr (eqrelrigtoring X) (rigtoringop2int X (rigtoringunel2int X) x) = setquotpr (eqrelrigtoring X) x). apply (maponpaths (setquotpr (eqrelrigtoring X))). unfold rigtoringop2int. simpl. induction x as [ x1 x2 ]. simpl. set (lu2 := riglunax2 X). set (ru1 := rigrunax1 X). set (m0x := rigmult0x X). apply pathsdirprod. - rewrite (lu2 x1). rewrite (m0x x2). apply (ru1 x1). - rewrite (lu2 x2). rewrite (m0x x1). apply (ru1 x2). Qed.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.