Lemma plusNonnegativeRationals_lecompat_l : ∏ r q n : NonnegativeRationals, (q <= n) <-> (r + q <= r + n). Proof. intros r q n. rewrite ! (iscomm_plusNonnegativeRationals r). now apply plusNonnegativeRationals_lecompat_r. 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.