proposition: Lemma Dcuts_of_Dcuts'_open : ∏ (x : Dcuts), Dcuts_of_Dcuts'_val x -> hexists (λ y : Dcuts, (Dcuts_of_Dcuts'_val y) × (x < y)).
proof: 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.
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