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