Lemma isinvringmultgttoislinvringmultgt (X : ring) {R : hrel X} (is0 : @isbinophrel X R) (is : isinvringmultgt X R) : ∏ a b c : X, R c 0 → R (c * a) (c * b) → R a b. Proof. intros a b c rc0 r. set (rab':= (pr2 is0) _ _ (c * - b) r). clearbody rab'. change (pr1 (R (c * a + c * - b) (c * b + c * - b))) in rab'. rewrite <- (ringldistr X _ _ c) in rab'. rewrite <- (ringldistr X _ _ c) in rab'. rewrite (ringrinvax1 X b) in rab'. rewrite (ringmultx0 X _) in rab'. set (r' := (pr1 is) _ _ rab' rc0). clearbody r'. set (r'' := (pr2 is0) _ _ b r'). clearbody r''. change (pr1 (R (a - b + b) (0 + b))) in r''. rewrite (ringlunax1 X _) in r''. rewrite (ringassoc1 X a _ _) in r''. rewrite (ringlinvax1 X b) in r''. rewrite (ringrunax1 X _) in r''. apply r''. Qed.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.