Lemma hr_mult_ltcompat_l' : ∏ x y z : hr_commring, hr_le_rel 0%ring x -> hr_lt_rel (y * x)%ring (z * x)%ring -> hr_lt_rel y z. Proof. intros X Y Z Hx0. apply_pr2_in hr_to_NR_nonnegative Hx0. rewrite <- (hr_to_NR_bij X), <- (hr_to_NR_bij Y), <- (hr_to_NR_bij Z). rewrite !NR_to_hr_mult ; simpl pr1 ; simpl pr2. change (pr2 (hr_to_NR X)) with (hr_to_NRneg X). rewrite Hx0. rewrite !israbsorb_zero_multNonnegativeReals, !isrunit_zero_plusNonnegativeReals, !islunit_zero_plusNonnegativeReals. intros Hlt. apply NR_to_hr_lt. apply multNonnegativeReals_ltcompat_l' with (pr1 (hr_to_NR X)). rewrite !isrdistr_plus_multNonnegativeReals. 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.