proposition: 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: 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 (pathsinv0 (ringldistr X _ _ c)) in rab'. rewrite (pathsinv0 (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''. Defined.
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids