Lemma isringmultgttoislringmultgt (X : ring) {R : hrel X} (is0 : @isbinophrel X R) (is : isringmultgt X R) : ∏ a b c : X, R c 0 → R a b → R (c * a) (c * b). Proof. intros a b c rc0 rab. set (rab':= (pr2 is0) _ _ (- b) rab). clearbody rab'. change (pr1 (R (a - b) (b - b))) in rab'. rewrite (ringrinvax1 X b) in rab'. set (r' := is _ _ rc0 rab'). clearbody r'. set (r'' := (pr2 is0) _ _ (c * b) r'). clearbody r''. change (pr1 (R (c * (a - b) + c * b) (0 + c * b))) in r''. rewrite (ringlunax1 X _) in r''. rewrite <- (ringldistr X _ _ c) 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.