Lemma NRNRtoR_ap : ∏ x x' y y' : NonnegativeReals, (x + y' ≠ x' + y)%NR <-> NRNRtoR x y ≠ NRNRtoR x' y'. Proof. intros x x' y y'. apply (NR_to_hr_ap (x,,y) (x' ,, y')). 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.