proposition: Lemma rigtoringldistr (X : rig) : isldistr (rigtoringop1 X) (rigtoringop2 X).
proof: Proof. unfold isldistr. apply (setquotuniv3prop _ (λ x x' x'', _ = _)). intros x x' x''. change (paths (setquotpr (eqrelrigtoring X) (rigtoringop2int X x'' (rigtoringop1int X x x'))) (setquotpr (eqrelrigtoring X) (rigtoringop1int X (rigtoringop2int X x'' x) (rigtoringop2int X x'' x')))). apply (maponpaths (setquotpr (eqrelrigtoring X))). unfold rigtoringop1int. unfold rigtoringop2int. simpl. set (ld := rigldistr X). set (cm1 := rigcomm1 X). set (rr := abmonoidoprer (rigop1axs X)). apply pathsdirprod. - rewrite (ld _ _ (pr1 x'')). rewrite (ld _ _ (pr2 x'')). apply (rr _ (pr1 x'' * pr1 x') (pr2 x'' * pr2 x) _). - rewrite (ld _ _ (pr1 x'')). rewrite (ld _ _ (pr2 x'')). apply (rr _ (pr1 x'' * pr2 x') (pr2 x'' * pr1 x) _). Defined.
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids