proposition: 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: Proof. intros. intros a b ra rb. set (int := is b 0 a ra rb). clearbody int. rewrite (ringmultx0 X _) in int. apply int. Defined.
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids