proposition: Lemma isinvringrigtoringmultgt (X : rig) {R : hrel X} (is0 : @isbinophrel (rigaddabmonoid X) R) (is1 : @isinvbinophrel (rigaddabmonoid X) R) (is : isinvrigmultgt X R) : isinvringmultgt (rigtoring X) (rigtoringrel X is0).
proof: Proof. intros. split. - assert (int : ∏ a b, isaprop (rigtoringrel X is0 (a * b) ringunel1 -> rigtoringrel X is0 a ringunel1 -> rigtoringrel X is0 b ringunel1)). intros. apply impred. intro. apply impred. intro. apply (pr2 _). apply (setquotuniv2prop _ (λ a b, make_hProp _ (int a b))). intros xa1 xa2. change ((abgrdiffrelint (rigaddabmonoid X) R (@rigtoringop2int X xa1 xa2) (make_dirprod (@rigunel1 X) (@rigunel1 X))) -> (abgrdiffrelint (rigaddabmonoid X) R) xa1 (make_dirprod (@rigunel1 X) (@rigunel1 X)) -> (abgrdiffrelint (rigaddabmonoid X) R) xa2 (make_dirprod (@rigunel1 X) (@rigunel1 X))). unfold abgrdiffrelint. simpl. apply hinhfun2. intros t22 t21. set (c2 := pr1 t22). set (c1 := pr1 t21). set (r1 := pr2 t21). set (r2 := pr2 t22). set (x1 := pr1 xa1). set (a1 := pr2 xa1). set (x2 := pr1 xa2). set (a2 := pr2 xa2). simpl in r2. clearbody r2. change (pr1 (R (x1 * x2 + a1 * a2 + 0 + c2) (0 + (x1 * a2 + a1 * x2) + c2))) in r2. rewrite (riglunax1 X _) in r2. rewrite (rigrunax1 X _) in r2. rewrite (rigrunax1 X _). rewrite (riglunax1 X _). set (r2' := (pr2 is1) _ _ c2 r2). clearbody r1. change (pr1 (R (x1 + 0 + c1) (0 + a1 + c1))) in r1. rewrite (riglunax1 X _) in r1. rewrite (rigrunax1 X _) in r1. set (r1' := (pr2 is1) _ _ c1 r1). split with 0. rewrite (rigrunax1 X _). rewrite (rigrunax1 X _). apply ((pr1 is) _ _ _ _ r2' r1'). - assert (int : ∏ a b, isaprop (rigtoringrel X is0 (a * b) ringunel1 -> rigtoringrel X is0 b ringunel1 -> rigtoringrel X is0 a ringunel1)). intros. apply impred. intro. apply impred. intro. apply (pr2 _). apply (setquotuniv2prop _ (λ a b, make_hProp _ (int a b))). intros xa1 xa2. change ((abgrdiffrelint (rigaddabmonoid X) R (@rigtoringop2int X xa1 xa2) (make_dirprod (@rigunel1 X) (@rigunel1 X))) -> (abgrdiffrelint (rigaddabmonoid X) R) xa2 (make_dirprod (@rigunel1 X) (@rigunel1 X)) -> (abgrdiffrelint (rigaddabmonoid X) R) xa1 (make_dirprod (@rigunel1 X) (@rigunel1 X))). unfold abgrdiffrelint. simpl. apply hinhfun2. intros t22 t21. set (c2 := pr1 t22). set (c1 := pr1 t21). set (r1 := pr2 t21). set (r2 := pr2 t22). set (x1 := pr1 xa1). set (a1 := pr2 xa1). set (x2 := pr1 xa2). set (a2 := pr2 xa2). simpl in r2. clearbody r2. change (pr1 (R (x1 * x2 + a1 * a2 + 0 + c2) (0 + (x1 * a2 + a1 * x2) + c2))) in r2. rewrite (riglunax1 X _) in r2. rewrite (rigrunax1 X _) in r2. rewrite (rigrunax1 X _). rewrite (riglunax1 X _). set (r2' := (pr2 is1) _ _ c2 r2). clearbody r1. change (pr1 (R (x2 + 0 + c1) (0 + a2 + c1))) in r1. rewrite (riglunax1 X _) in r1. rewrite (rigrunax1 X _) in r1. set (r1' := (pr2 is1) _ _ c1 r1). split with 0. rewrite (rigrunax1 X _). rewrite (rigrunax1 X _). apply ((pr2 is) _ _ _ _ r2' r1'). Defined.
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids