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