proposition: Lemma iscomprelfun_hr_to_NR : iscomprelfun (Y := NonnegativeReals × NonnegativeReals) (binopeqrelabgrdiff (rigaddabmonoid NonnegativeReals)) (λ x : NonnegativeReals × NonnegativeReals, pr1 x - pr2 x ,, pr2 x - pr1 x).
proof: 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.
imports: UniMath.Algebra.Groups UniMath.Foundations.Preamble UniMath.MoreFoundations.Orders UniMath.MoreFoundations.Tactics UniMath.OrderTheory.Lattice.Lattice UniMath.RealNumbers.Prelim UniMath.RealNumbers.Sets UniMath.RealNumbers.NonnegativeRationals UniMath.RealNumbers.NonnegativeReals