Definition hr_to_NR (x : hr_commring) : NonnegativeReals × NonnegativeReals. Proof. revert x. simple refine (setquotuniv _ (_,,_) _ _). - apply isasetdirprod ; apply (pr2 (pr1 (pr1 (pr1 NonnegativeReals)))). - intros x. apply (pr1 x - pr2 x ,, pr2 x - pr1 x). - apply iscomprelfun_hr_to_NR. Defined.
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.