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