Lemma iscomprelfun_hr_to_NR : iscomprelfun (Y := NonnegativeReals × NonnegativeReals) (binopeqrelabgrdiff (rigaddabmonoid NonnegativeReals)) (λ x : NonnegativeReals × NonnegativeReals, pr1 x - pr2 x ,, pr2 x - pr1 x). Proof. intros x y. apply factor_through_squash. { refine (isasetdirprod _ _ _ _ _ _) ; apply (pr2 (pr1 (pr1 (pr1 NonnegativeReals)))). } intros c. apply dirprodeq. + apply iscomprelfun_NRminus. apply (plusNonnegativeReals_eqcompat_l (pr1 c)). exact (pr2 c). + apply (iscomprelfun_NRminus (pr2 x ,, pr1 x) (pr2 y ,, pr1 y)). simpl. rewrite (iscomm_plusNonnegativeReals (pr2 x)), (iscomm_plusNonnegativeReals (pr2 y)). apply (plusNonnegativeReals_eqcompat_l (pr1 c)), pathsinv0. exact (pr2 c). Qed.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.RealNumbers.Prelim. Require Import UniMath.RealNumbers.Sets. Require Import UniMath.RealNumbers.NonnegativeRationals.