proposition: 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: 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.
imports: UniMath.MoreFoundations.Orders UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Notations UniMath.RealNumbers.Sets UniMath.Algebra.ConstructiveStructures UniMath.OrderTheory.Lattice.Lattice UniMath.RealNumbers.Prelim UniMath.RealNumbers.NonnegativeRationals