proposition: Lemma rigtoringlunit2 (X : rig) : islunit (rigtoringop2 X) (rigtoringunel2 X).
proof: Proof. unfold islunit. apply (setquotunivprop _ (λ x, _ = _)). intro x. change (paths (setquotpr (eqrelrigtoring X) (rigtoringop2int X (rigtoringunel2int X) x)) (setquotpr (eqrelrigtoring X) x)). apply (maponpaths (setquotpr (eqrelrigtoring X))). unfold rigtoringop2int. simpl. destruct 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). Defined.
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids