Lemma isringrigtoringmultgt (X : rig) {R : hrel X} (is0 : @isbinophrel (rigaddabmonoid X) R) (is : isrigmultgt X R) : isringmultgt (rigtoring X) (rigtoringrel X is0). Proof. intros. set (assoc := rigassoc1 X). set (comm := rigcomm1 X). set (rer := (abmonoidrer (rigaddabmonoid X)) : ∏ a b c d : X, (a + b) + (c + d) = (a + c) + (b + d)). set (ld := rigldistr X). set (rd := rigrdistr X). assert (int : ∏ a b, isaprop (rigtoringrel X is0 a ringunel1 → rigtoringrel X is0 b ringunel1 → rigtoringrel X is0 (a * b) ringunel1)). { intros a b. apply impred. intro. apply impred. intro. apply (pr2 _). } unfold isringmultgt. apply (setquotuniv2prop _ (λ a b, make_hProp _ (int a b))). intros xa1 xa2. change ((abgrdiffrelint (rigaddabmonoid X) R) xa1 (@rigunel1 X ,, @rigunel1 X) → (abgrdiffrelint (rigaddabmonoid X) R) xa2 (@rigunel1 X ,, @rigunel1 X) → (abgrdiffrelint (rigaddabmonoid X) R (@rigtoringop2int X xa1 xa2) (@rigunel1 X ,, @rigunel1 X))). unfold abgrdiffrelint. simpl. apply hinhfun2. intros t22 t21. set (c2 := pr1 t21). set (c1 := pr1 t22). set (r1 := pr2 t21). set (r2 := pr2 t22). set (x1 := pr1 xa1). set (a1 := pr2 xa1). set (x2 := pr1 xa2). set (a2 := pr2 xa2). exists ((x1 * c2 + a1 * c2) + ((c1 * x2 + c1 * c2) + (c1 * a2 + c1 * c2))). change (pr1 (R (x1 * x2 + a1 * a2 + 0 + ((x1 * c2 + a1 * c2) + ((c1 * x2 + c1 * c2) + (c1 * a2 + c1 * c2)))) (0 + (x1 * a2 + a1 * x2) + (x1 * c2 + a1 * c2 + ((c1 * x2 + c1 * c2) + (c1 * a2 + c1 * c2)))))). rewrite (riglunax1 X _). rewrite (rigrunax1 X _). rewrite (assoc (x1 * c2) _ _). rewrite (rer _ (a1 * a2) _ _). rewrite (rer _ (a1 * x2) _ _). rewrite <- (assoc (a1 * a2) _ _). rewrite <- (assoc (a1 * x2) _ _). rewrite <- (assoc (x1 * x2 + _) _ _). rewrite <- (assoc (x1 * a2 + _) _ _). rewrite (rer _ (a1 * a2 + _) _ _). rewrite (rer _ (a1 * x2 + _) _ _). rewrite <- (ld _ _ x1). rewrite <- (ld _ _ x1). rewrite <- (ld _ _ c1). rewrite <- (ld _ _ c1). rewrite <- (ld _ _ a1). rewrite <- (ld _ _ a1). rewrite <- (rd _ _ (x2 + c2)). rewrite <- (rd _ _ (a2 + c2)). rewrite (comm (a1 * _) _). rewrite (rer _ (c1 * _) _ _). rewrite <- (rd _ _ (x2 + c2)). rewrite <- (rd _ _ (a2 + c2)). clearbody r1. clearbody r2. change (pr1 (R (x2 + 0 + c2) (0 + a2 + c2))) in r1. change (pr1 (R (x1 + 0 + c1) (0 + a1 + c1))) in r2. rewrite (rigrunax1 X _) in r1. rewrite (riglunax1 X _) in r1. rewrite (rigrunax1 X _) in r2. rewrite (riglunax1 X _) in r2. rewrite (comm c1 a1). apply (is _ _ _ _ r2 r1). Qed.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.