Lemma rigtoringldistr (X : rig) : isldistr (rigtoringop1 X) (rigtoringop2 X). Proof. unfold isldistr. apply (setquotuniv3prop _ (λ x x' x'', _ = _)). intros x x' x''. change (setquotpr (eqrelrigtoring X) (rigtoringop2int X x'' (rigtoringop1int X x x')) = setquotpr _ (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) _). Qed.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.