Lemma hr_plus_ltcompat_l : ∏ x y z : hr_commring, hr_lt_rel y z <-> hr_lt_rel (y+x)%ring (z+x)%ring. Proof. intros X Y Z. rewrite <- (hr_to_NR_bij X), <- (hr_to_NR_bij Y), <- (hr_to_NR_bij Z). rewrite !NR_to_hr_plus. split ; intro Hlt. - apply NR_to_hr_lt ; simpl. rewrite !(iscomm_plusNonnegativeReals _ (pr1 (hr_to_NR X))), !isassoc_plusNonnegativeReals. apply plusNonnegativeReals_ltcompat_r. rewrite <- ! isassoc_plusNonnegativeReals. apply plusNonnegativeReals_ltcompat_l. now apply_pr2 NR_to_hr_lt. - apply NR_to_hr_lt ; simpl. apply_pr2 (plusNonnegativeReals_ltcompat_l (pr2 (hr_to_NR X))). apply_pr2 (plusNonnegativeReals_ltcompat_r (pr1 (hr_to_NR X))). rewrite <- ! isassoc_plusNonnegativeReals. rewrite !(iscomm_plusNonnegativeReals (pr1 (hr_to_NR X))), !(isassoc_plusNonnegativeReals (_ + pr1 (hr_to_NR X))). now apply_pr2_in NR_to_hr_lt Hlt. 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.