proposition: 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: 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.
imports: UniMath.Algebra.Groups UniMath.Foundations.Preamble UniMath.MoreFoundations.Orders UniMath.MoreFoundations.Tactics UniMath.OrderTheory.Lattice.Lattice UniMath.RealNumbers.Prelim UniMath.RealNumbers.Sets UniMath.RealNumbers.NonnegativeRationals UniMath.RealNumbers.NonnegativeReals