Lemma isOneSided_Dcuts_open : ∏ D, isOneSided D → Dcuts_def_open (λ r, D (pr1 r)). Proof. intros D H r Dr. generalize ((pr1 (pr2 H)) (pr1 r) Dr). apply hinhfun. intros q. assert (Hq : 0 <= pr1 q). { apply istranshqleh with (pr1 r). { exact (pr2 r). } apply hqlthtoleh, (pr2 (pr2 q)). } exists (pr1 q,,Hq). split. - change (D (NonnegativeRationals_to_Rationals (pr1 q,,Hq))). exact (pr1 (pr2 q)). - rewrite ltNonnegativeRationals_correct. change (pr1 r < (NonnegativeRationals_to_Rationals (pr1 q,,Hq))). exact (pr2 (pr2 q)). Qed.
Require Import UniMath.RealNumbers.Prelim. Require Import UniMath.RealNumbers.NonnegativeRationals. Require Import UniMath.RealNumbers.NonnegativeReals.