proposition: Lemma rigtoringassoc2 (X : rig) : isassoc (rigtoringop2 X).
proof: Proof. unfold isassoc. apply (setquotuniv3prop _ (λ x x' x'', _ = _)). intros x x' x''. change (paths (setquotpr (eqrelrigtoring X) (rigtoringop2int X (rigtoringop2int X x x') x'')) (setquotpr (eqrelrigtoring X) (rigtoringop2int X x (rigtoringop2int X x' x'')))). apply (maponpaths (setquotpr (eqrelrigtoring X))). unfold rigtoringop2int. simpl. set (rd := rigrdistr X). set (ld := rigldistr X). set (cm1 := rigcomm1 X). set (as1 := rigassoc1 X). set (as2 := rigassoc2 X). set (rr := abmonoidoprer (rigop1axs X)). apply pathsdirprod. rewrite (rd _ _ (pr1 x'')). rewrite (rd _ _ (pr2 x'')). rewrite (ld _ _ (pr1 x)). rewrite (ld _ _ (pr2 x)). destruct (as2 (pr1 x) (pr1 x') (pr1 x'')). destruct (as2 (pr1 x) (pr2 x') (pr2 x'')). destruct (as2 (pr2 x) (pr1 x') (pr2 x'')). destruct (as2 (pr2 x) (pr2 x') (pr1 x'')). destruct (cm1 (pr2 x * pr2 x' * pr1 x'') (pr2 x * pr1 x' * pr2 x'')). rewrite (rr _ (pr2 x * pr2 x' * pr1 x'') (pr1 x * pr2 x' * pr2 x'') _). apply idpath. rewrite (rd _ _ (pr1 x'')). rewrite (rd _ _ (pr2 x'')). rewrite (ld _ _ (pr1 x)). rewrite (ld _ _ (pr2 x)). destruct (as2 (pr1 x) (pr1 x') (pr2 x'')). destruct (as2 (pr1 x) (pr2 x') (pr1 x'')). destruct (as2 (pr2 x) (pr1 x') (pr1 x'')). destruct (as2 (pr2 x) (pr2 x') (pr2 x'')). destruct (cm1 (pr2 x * pr2 x' * pr2 x'') (pr2 x * pr1 x' * pr1 x'')). rewrite (rr _ (pr1 x * pr2 x' * pr1 x'') (pr2 x * pr2 x' * pr2 x'') _). apply idpath. Defined.
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids