Lemma islringmultgttoisringmultgt (X : ring) {R : hrel X} (is : ∏ a b c : X, R c 0 → R a b → R (c * a) (c * b)) : isringmultgt X R. Proof. intros. intros a b ra rb. set (int := is b 0 a ra rb). clearbody int. rewrite (ringmultx0 X _) in int. apply int. Qed.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.