Lemma RtoNRNR_NRNRtoR : ∏ x y : NonnegativeReals, (RtoNRNR (NRNRtoR x y)) = ((x - y)%NR ,, (y - x)%NR). Proof. intros X Y. unfold RtoNRNR, NRNRtoR. unfold hr_to_NR, NR_to_hr. now rewrite setquotunivcomm. 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.