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