Lemma Dcuts_of_Dcuts_open : ∏ (x : NonnegativeRationals), Dcuts_of_Dcuts_val x -> hexists (λ y : NonnegativeRationals, (Dcuts_of_Dcuts_val y) × (x < y)%NRat). Proof. intros r. apply hinhuniv ; intros X. generalize (is_Dcuts_open _ _ (pr2 (pr2 X))). apply hinhfun ; intros n. exists (pr1 n) ; split. - apply hinhpr. exists (pr1 X) ; split. + exact (pr1 (pr2 X)). + exact (pr1 (pr2 n)). - exact (pr2 (pr2 n)). 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.