proposition: Lemma hr_mult_lecompat_l' : ∏ x y z : hr_commring, hr_lt_rel 0%ring x -> hr_le_rel (y * x)%ring (z * x)%ring -> hr_le_rel y z.
proof: Proof. intros x y z Hx0 Hle. apply hr_notlt_le. apply_pr2_in hr_notlt_le Hle. intro Hlt ; apply Hle. apply (hr_mult_ltcompat_l x). - exact Hx0. - exact 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