Lemma rigtoringrdistr (X : rig) : isrdistr (rigtoringop1 X) (rigtoringop2 X). Proof. unfold isrdistr. apply (setquotuniv3prop _ (λ x x' x'', _ = _)). intros x x' x''. change (setquotpr (eqrelrigtoring X) (rigtoringop2int X (rigtoringop1int X 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 (rd := rigrdistr X). set (cm1 := rigcomm1 X). set (rr := abmonoidoprer (rigop1axs X)). apply pathsdirprod. - rewrite (rd _ _ (pr1 x'')). rewrite (rd _ _ (pr2 x'')). apply (rr _ (pr1 x' * pr1 x'') (pr2 x * pr2 x'') _). - rewrite (rd _ _ (pr1 x'')). rewrite (rd _ _ (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.