proposition: Lemma rigtoringrdistr (X : rig) : isrdistr (rigtoringop1 X) (rigtoringop2 X).
proof: Proof. unfold isrdistr. apply (setquotuniv3prop _ (λ x x' x'', _ = _)). intros x x' x''. change (paths (setquotpr (eqrelrigtoring X) (rigtoringop2int X (rigtoringop1int X 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 (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'') _). Defined.
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids