Lemma multNonnegativeRationals_lecompat_l' : ∏ k x y : NonnegativeRationals, 0 < k -> k * x <= k * y -> x <= y. Proof. intros k x y Hk0. apply (hqlehandmultlinv (pr1 x) (pr1 y) (pr1 k)). exact Hk0. Qed.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.RealNumbers.Sets. Require Import UniMath.RealNumbers.Fields. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.RealNumbers.Prelim.