proposition: Lemma hr_mult_ltcompat_l : ∏ x y z : hr_commring, hr_lt_rel 0%ring x -> hr_lt_rel y z -> hr_lt_rel (y * x)%ring (z * x)%ring.
proof: Proof. intros X Y Z Hx0 Hlt. apply_pr2_in hr_to_NR_positive 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 (pr2 Hx0). rewrite !israbsorb_zero_multNonnegativeReals, !isrunit_zero_plusNonnegativeReals, !islunit_zero_plusNonnegativeReals. apply NR_to_hr_lt ; simpl. rewrite <- !isrdistr_plus_multNonnegativeReals. apply multNonnegativeReals_ltcompat_l. - apply ispositive_apNonnegativeReals. exact (pr1 Hx0). - apply_pr2 NR_to_hr_lt. now rewrite !hr_to_NR_bij. 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