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. intros. intros a b ra rb. set (ax0 := (pr2 (pr1 (pr2 f))) : (f 0) = 0). set (ax1 := (pr1 (pr2 (pr2 f))) : ∏ a b, f (a * b) = f a * f b). rewrite ax0 in ra. rewrite ax0 in rb. rewrite ax0. rewrite (ax1 _ _). apply (isr _ _ ra rb). Defined.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.