Lemma isinvringmultgttoisinvrigmultgt (X : ring) {R : hrel X} (is0 : @isbinophrel X R) (is : isinvringmultgt X R) : isinvrigmultgt X R. Proof. intros. set (rer := abmonoidrer X). simpl in rer. split. - intros a b c d r rab. set (r' := (pr2 is0) _ _ (a * - d + - b * c) r). clearbody r'. simpl in r'. rewrite (rer _ (b * c) _ _) in r'. rewrite <- (ringldistr X _ _ a) in r'. rewrite <- (ringrdistr X _ _ c) in r'. rewrite (ringrinvax1 X d) in r'. rewrite (ringrinvax1 X b) in r'. rewrite (ringmult0x X _) in r'. rewrite (ringmultx0 X _) in r'. rewrite (ringlunax1 X) in r'. rewrite (rer _ (b * d) _ _) in r'. rewrite <- (ringldistr X _ _ a) in r'. simpl in r'. fold pr1ring in r'. change (pr1 X) with (pr1ring X) in r'. rewrite <- (ringmultminusminus X b d) in r'. rewrite <- (ringldistr X _ _ (- b)) in r'. rewrite (ringcomm1 X _ c) in r'. rewrite <- (ringrdistr X _ _ _) in r'. set (rab' := (pr2 is0) _ _ (- b) rab). clearbody rab'. simpl in rab'. rewrite (ringrinvax1 X b) in rab'. set (rcd' := (pr1 is) _ _ r' rab'). set (rcd'' := (pr2 is0) _ _ d rcd'). simpl in rcd''. rewrite (ringassoc1 _ _ _) in rcd''. rewrite (ringlinvax1 X _) in rcd''. rewrite (ringlunax1 X _) in rcd''. rewrite (ringrunax1 X _) in rcd''. apply rcd''. - intros a b c d r rcd. set (r' := (pr2 is0) _ _ (a * - d + - b * c) r). clearbody r'. simpl in r'. rewrite (rer _ (b * c) _ _) in r'. rewrite <- (ringldistr X _ _ a) in r'. rewrite <- (ringrdistr X _ _ c) in r'. rewrite (ringrinvax1 X d) in r'. rewrite (ringrinvax1 X b) in r'. rewrite (ringmult0x X _) in r'. rewrite (ringmultx0 X _) in r'. rewrite (ringlunax1 X) in r'. rewrite (rer _ (b * d) _ _) in r'. rewrite <- (ringldistr X _ _ a) in r'. simpl in r'. fold pr1ring in r'. change (pr1 X) with (pr1ring X) in r'. rewrite <- (ringmultminusminus X b d) in r'. rewrite <- (ringldistr X _ _ (- b)) in r'. rewrite (ringcomm1 X _ c) in r'. rewrite <- (ringrdistr X _ _ _) in r'. set (rcd' := (pr2 is0) _ _ (- d) rcd). clearbody rcd'. simpl in rcd'. rewrite (ringrinvax1 X d) in rcd'. set (rab' := (pr2 is) _ _ r' rcd'). set (rab'' := (pr2 is0) _ _ b rab'). simpl in rab''. rewrite (ringassoc1 _ _ _) in rab''. rewrite (ringlinvax1 X _) in rab''. rewrite (ringlunax1 X _) in rab''. rewrite (ringrunax1 X _) in rab''. apply rab''. Qed.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.