Lemma isringmultgttoisrigmultgt (X : ring) {R : hrel X} (is0 : @isbinophrel X R) (is : isringmultgt X R) : isrigmultgt X R. Proof. intros. set (rer := abmonoidrer X). simpl in rer. intros a b c d rab rcd. assert (intab : R (a - b) 0). { induction (ringrinvax1 X b). apply ((pr2 is0) _ _ (- b)). apply rab. } assert (intcd : R (c - d) 0). { induction (ringrinvax1 X d). apply ((pr2 is0) _ _ (- d)). apply rcd. } set (int := is _ _ intab intcd). rewrite (ringrdistr X _ _ _) in int. rewrite (ringldistr X _ _ _) in int. rewrite (ringldistr X _ _ _) in int. set (int' := (pr2 is0) _ _ (a * d + b * c) int). clearbody int'. simpl in int'. rewrite (ringlunax1 _) in int'. rewrite (ringcomm1 X (- b * c) _) in int'. rewrite (rer _ (a * - d) _ _) in int'. rewrite (ringassoc1 X _ (a * - d + - b * c) _) in int'. rewrite (rer _ _ (a * d) _) in int'. rewrite <- (ringldistr X _ _ a) in int'. rewrite (ringlinvax1 X d) in int'. rewrite (ringmultx0 X _) in int'. rewrite <- (ringrdistr X _ _ c) in int'. rewrite (ringlinvax1 X b) in int'. rewrite (ringmult0x X _) in int'. rewrite (ringrunax1 X _) in int'. rewrite (ringrunax1 X _) in int'. rewrite (ringmultminusminus X b d) in int'. apply int'. Qed.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.