Lemma Dcuts_def_corr_not_empty (X : hsubtype NonnegativeRationals) : X 0 -> Dcuts_def_corr X -> ∏ c : NonnegativeRationals, (0 < c)%NRat -> ∃ x : NonnegativeRationals, X x × ¬ X (x + c). Proof. intros X0 Hx c Hc. generalize (Hx c Hc). apply hinhuniv ; apply sumofmaps ; [intros nXc | intros Hx' ]. - apply hinhpr ; exists 0%NRat ; split. + exact X0. + rewrite islunit_zeroNonnegativeRationals. exact nXc. - apply hinhpr ; exact Hx'. 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.