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