proposition: Lemma Dcuts_of_Dcuts_open : ∏ (x : NonnegativeRationals), Dcuts_of_Dcuts_val x -> hexists (λ y : NonnegativeRationals, (Dcuts_of_Dcuts_val y) × (x < y)%NRat).
proof: 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.
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