proposition: 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: 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.
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