Lemma plusNonnegativeRationals_le_r : ∏ r q : NonnegativeRationals, r <= r + q. Proof. intros r q. pattern r at 1. rewrite <- (isrunit_zeroNonnegativeRationals r). apply hqlehandplusl. apply (pr2 q). 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.