Lemma plusNonnegativeRationals_lecompat_r : ∏ r q n : NonnegativeRationals, (q <= n) <-> (q + r <= n + r). Proof. intros r q n. split. - now apply hqlehandplusr. - now apply hqlehandplusrinv. 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.