proposition: 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: 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.
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