Lemma hr_to_NRpos_minus : ∏ x y : hr_commring, hr_to_NRpos x - hr_to_NRpos y <= hr_to_NRpos (x - y)%ring. Proof. intros X Y. set (x := hr_to_NRpos X) ; set (y := hr_to_NRpos Y). rewrite <- (hr_to_NR_bij X), <- (hr_to_NR_bij Y). rewrite NR_to_hr_minus. change (pr1 (hr_to_NR X)) with x. change (pr1 (hr_to_NR Y)) with y. change (pr2 (hr_to_NR X)) with (hr_to_NRneg X). change (pr2 (hr_to_NR Y)) with (hr_to_NRneg Y). rewrite hr_to_NRpos_NR_to_hr. simpl pr1 ; simpl pr2. apply_pr2 (plusNonnegativeReals_lecompat_l (hr_to_NRneg X + y)). rewrite <- maxNonnegativeReals_minus_plus. rewrite (iscomm_plusNonnegativeReals _ y), <- isassoc_plusNonnegativeReals, <- maxNonnegativeReals_minus_plus. rewrite isrdistr_max_plusNonnegativeReals. apply maxNonnegativeReals_le. - rewrite <- max_plusNonnegativeReals. + apply maxNonnegativeReals_le. * eapply istrans_leNonnegativeReals, maxNonnegativeReals_le_l. apply plusNonnegativeReals_le_l. * eapply istrans_leNonnegativeReals, maxNonnegativeReals_le_r. apply plusNonnegativeReals_le_r. + apply hr_to_NRposneg_zero. - apply maxNonnegativeReals_le_r. 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.