proposition: Lemma isringrigtoringmultgt (X : rig) {R : hrel X} (is0 : @isbinophrel (rigaddabmonoid X) R) (is : isrigmultgt X R) : isringmultgt (rigtoring X) (rigtoringrel X is0).
proof: Proof. intros. set (assoc := rigassoc1 X). set (comm := rigcomm1 X). set (rer := (abmonoidrer (rigaddabmonoid X)) : ∏ a b c d : X, paths ((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 (make_dirprod (@rigunel1 X) (@rigunel1 X)) -> (abgrdiffrelint (rigaddabmonoid X) R) xa2 (make_dirprod (@rigunel1 X) (@rigunel1 X)) -> (abgrdiffrelint (rigaddabmonoid X) R (@rigtoringop2int X xa1 xa2) (make_dirprod (@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). split with ((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 (pathsinv0 (assoc (a1 * a2) _ _)). rewrite (pathsinv0 (assoc (a1 * x2) _ _)). rewrite (pathsinv0 (assoc (x1 * x2 + _) _ _)). rewrite (pathsinv0 (assoc (x1 * a2 + _) _ _)). rewrite (rer _ (a1 * a2 + _) _ _). rewrite (rer _ (a1 * x2 + _) _ _). rewrite (pathsinv0 (ld _ _ x1)). rewrite (pathsinv0 (ld _ _ x1)). rewrite (pathsinv0 (ld _ _ c1)). rewrite (pathsinv0 (ld _ _ c1)). rewrite (pathsinv0 (ld _ _ a1)). rewrite (pathsinv0 (ld _ _ a1)). rewrite (pathsinv0 (rd _ _ (x2 + c2))). rewrite (pathsinv0 (rd _ _ (a2 + c2))). rewrite (comm (a1 * _) _). rewrite (rer _ (c1 * _) _ _). rewrite (pathsinv0 (rd _ _ (x2 + c2))). rewrite (pathsinv0 (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). Defined.
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids