Lemma hr_to_NRneg_NR_to_hr_std : ∏ (x : NonnegativeReals × NonnegativeReals), (0 < pr1 x -> pr2 x = 0) -> hr_to_NRneg (NR_to_hr x) = pr2 x. Proof. intros x Hx. rewrite hr_to_NRneg_NR_to_hr. apply (plusNonnegativeReals_eqcompat_l (pr1 x)). rewrite <- maxNonnegativeReals_minus_plus. rewrite iscomm_plusNonnegativeReals, iscomm_maxNonnegativeReals. now apply max_plusNonnegativeReals. 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.