Lemma hr_to_NR_zero : hr_to_NR 0%ring = (0,,0). Proof. unfold ringunel1, unel_is ; simpl. unfold hr_to_NR. rewrite setquotunivcomm ; simpl. rewrite !minusNonnegativeReals_eq_zero. { reflexivity. } apply isrefl_leNonnegativeReals. 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.