proposition: Lemma isrigmultgttoisringmultgt (X : ring) {R : hrel X} (is : isrigmultgt X R) : isringmultgt X R.
proof: Proof. intros. intros a b ra0 rb0. set (is' := is _ _ _ _ ra0 rb0). simpl in is'. fold (pr1ring) in is'. rewrite 2? (ringmult0x X _) in is'. rewrite (ringmultx0 X _) in is'. rewrite 2? (ringrunax1 X _) in is'. exact is'. Defined.
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids