Lemma isrigmultgttoisringmultgt (X : ring) {R : hrel X} (is : isrigmultgt X R) : isringmultgt X R. 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'. Qed.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.