proposition: Lemma rigtoringop2comp (X : rig) : iscomprelrelfun2 (eqrelrigtoring X) (eqrelrigtoring X) (rigtoringop2int X).
proof: Proof. intros. apply iscomprelrelfun2if. - intros xx xx' aa. simpl. apply @hinhfun. intro tt1. destruct tt1 as [ x0 e ]. split with (x0 * pr2 aa + x0 * pr1 aa). set (rd := rigrdistr X). set (cm1 := rigcomm1 X). set (as1 := rigassoc1 X). set (rr := abmonoidoprer (rigop1axs X)). rewrite (cm1 (pr1 xx * pr1 aa) (pr2 xx * pr2 aa)). rewrite (rr _ (pr1 xx * pr1 aa) (pr1 xx' * pr2 aa) _). rewrite (cm1 (pr2 xx * pr2 aa) (pr1 xx' * pr2 aa)). destruct (rd (pr1 xx) (pr2 xx') (pr1 aa)). destruct (rd (pr1 xx') (pr2 xx) (pr2 aa)). rewrite (rr ((pr1 xx' + pr2 xx) * pr2 aa) ((pr1 xx + pr2 xx') * pr1 aa) (x0 * pr2 aa) (x0 * pr1 aa)). destruct (rd (pr1 xx' + pr2 xx) x0 (pr2 aa)). destruct (rd (pr1 xx + pr2 xx') x0 (pr1 aa)). rewrite (cm1 (pr1 xx' * pr1 aa) (pr2 xx' * pr2 aa)). rewrite (rr _ (pr1 xx' * pr1 aa) (pr1 xx * pr2 aa) _). rewrite (cm1 (pr2 xx' * pr2 aa) (pr1 xx * pr2 aa)). destruct (rd (pr1 xx') (pr2 xx) (pr1 aa)). destruct (rd (pr1 xx) (pr2 xx') (pr2 aa)). rewrite (rr ((pr1 xx + pr2 xx') * pr2 aa) ((pr1 xx' + pr2 xx) * pr1 aa) (x0 * pr2 aa) (x0 * pr1 aa)). destruct (rd (pr1 xx + pr2 xx') x0 (pr2 aa)). destruct (rd (pr1 xx' + pr2 xx) x0 (pr1 aa)). destruct e. apply idpath. - intros aa xx xx'. simpl. apply @hinhfun. intro tt1. destruct tt1 as [ x0 e ]. split with (pr1 aa * x0 + pr2 aa * x0). set (ld := rigldistr X). set (cm1 := rigcomm1 X). set (as1 := rigassoc1 X). set (rr := abmonoidoprer (rigop1axs X)). rewrite (rr _ (pr2 aa * pr2 xx) (pr1 aa * pr2 xx') _). destruct (ld (pr1 xx) (pr2 xx') (pr1 aa)). destruct (ld (pr2 xx) (pr1 xx') (pr2 aa)). rewrite (rr _ (pr2 aa * (pr2 xx + pr1 xx')) (pr1 aa * x0) _). destruct (ld (pr1 xx + pr2 xx') x0 (pr1 aa)). destruct (ld (pr2 xx + pr1 xx') x0 (pr2 aa)). rewrite (rr _ (pr2 aa * pr2 xx') (pr1 aa * pr2 xx) _). destruct (ld (pr1 xx') (pr2 xx) (pr1 aa)). destruct (ld (pr2 xx') (pr1 xx) (pr2 aa)). rewrite (rr _ (pr2 aa * (pr2 xx' + pr1 xx)) (pr1 aa * x0) _). destruct (ld (pr1 xx' + pr2 xx) x0 (pr1 aa)). destruct (ld (pr2 xx' + pr1 xx) x0 (pr2 aa)). rewrite (cm1 (pr2 xx) (pr1 xx')). rewrite (cm1 (pr2 xx') (pr1 xx)). destruct e. apply idpath. Defined.
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids