Lemma Dcuts_of_Dcuts'_open : ∏ (x : Dcuts), Dcuts_of_Dcuts'_val x -> hexists (λ y : Dcuts, (Dcuts_of_Dcuts'_val y) × (x < y)). Proof. intros r. apply hinhuniv. intros q. generalize (E_open _ (pr2 (pr2 q))). apply hinhfun. intros s. exists (NonnegativeRationals_to_Dcuts (pr1 s)). split. - apply hinhpr. exists (pr1 s). split. + simpl. now apply isirrefl_ltNonnegativeRationals. + exact (pr1 (pr2 s)). - apply hinhpr. exists (pr1 q). split. + exact (pr1 (pr2 q)). + simpl. exact (pr2 (pr2 s)). 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.