Lemma NR_to_hr_eq : ∏ x y : NonnegativeReals × NonnegativeReals, pr1 x + pr2 y = pr1 y + pr2 x <-> NR_to_hr x = NR_to_hr y. Proof. intros x y. split ; intros H. - apply iscompsetquotpr. apply hinhpr. exists 0. apply_pr2 plusNonnegativeReals_eqcompat_l. exact H. - generalize (invmap (weqpathsinsetquot _ _ _) H) ; clear H. apply factor_through_squash. { apply (pr2 (pr1 (pr1 (pr1 NonnegativeReals)))). } intros (c,p); generalize p; clear p. apply plusNonnegativeReals_eqcompat_l. 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.