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. intros. apply (binophrelandfun (ringaddfun f) R isr). Defined.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.