Lemma plusNonnegativeRationals_lt_r : ∏ r q : NonnegativeRationals, 0 < q -> r < r + q. Proof. intros x y Hy0. pattern x at 1. rewrite <- (isrunit_zeroNonnegativeRationals x). apply plusNonnegativeRationals_ltcompat_l. exact Hy0. 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.