proposition: Lemma ringaddhrelandfun {X Y : ring} (f : ringfun X Y) (R : hrel Y) (isr : @isbinophrel Y R) : @isbinophrel X (λ x x', R (f x) (f x')).
proof: Proof. intros. apply (binophrelandfun (ringaddfun f) R isr). Defined.
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids