Lemma Dcuts_zero_empty : ∏ r : NonnegativeRationals, neg (r ∈ 0). Proof. intros r ; simpl. change (neg (r < 0)%NRat). now apply isnonnegative_NonnegativeRationals'. Qed.
Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.RealNumbers.Sets. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.RealNumbers.Prelim. Require Import UniMath.RealNumbers.NonnegativeRationals.