proposition: Lemma ringmultgtandfun {X Y : ring} (f : ringfun X Y) (R : hrel Y) (isr : isringmultgt Y R) : isringmultgt X (λ x x', R (f x) (f x')).
proof: Proof. intros. intros a b ra rb. set (ax0 := (pr2 (pr1 (pr2 f))) : (f 0) = 0). set (ax1 := (pr1 (pr2 (pr2 f))) : ∏ a b, paths (f (a * b)) ((f a) * (f b))). rewrite ax0 in ra. rewrite ax0 in rb. rewrite ax0. rewrite (ax1 _ _). apply (isr _ _ ra rb). Defined.
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids