Lemma isDcuts_OneSided : ∏ (D : NonnegativeRationals → hProp), Dcuts_def_bot D → Dcuts_def_open D → Dcuts_def_corr D → isOneSided (λ q : hq, sumofmaps (λ _ : 0 > q, htrue) (λ Hq : 0 <= q, D (q,, Hq)) (hqgthorleh 0 q)). Proof. intros D Hbot Hopen Hcorr. split ; split. - apply hinhpr. exists (-(1)). induction (hqgthorleh 0 (- (1))) as [H | H]. + exact tt. + apply fromempty. refine (hqlehtoneghqgth _ _ _ _). * apply H. * apply hqgthandplusrinv with 1. rewrite hqlminus, hqplusl0. exact hq1_gt0. - generalize (Hcorr _ ispositive_oneNonnegativeRationals). apply hinhfun, sumofmaps ; intros H. + exists 1. induction (hqgthorleh 0 1) as [H0 | H0]. * apply fromempty. refine (hqgthtoneghqleh _ _ _ _). ** exact H0. ** exact hq1ge0. * assert (H1 : 1%NRat = (1 ,, H0)) by (apply subtypePath_prop ; reflexivity). rewrite H1 in H. exact H. + rename H into q. exists (pr1 (pr1 q) + 1). induction (hqgthorleh 0 (pr1 (pr1 q) + 1)) as [H0 | H0]. * apply fromempty. refine (hqgthtoneghqleh _ _ _ _). ** apply H0. ** apply hq0lehandplus. *** exact (pr2 (pr1 q)). *** exact hq1ge0. * assert (Hq1 : (pr1 q + 1)%NRat = (pr1 (pr1 q) + 1 ,, H0)) by (apply subtypePath_prop ; reflexivity). generalize (pr2 (pr2 q)) ; intro Hq. rewrite Hq1 in Hq. exact Hq. - intros r Dr. induction (hqgthorleh 0 r) as [Hr | Hr]. + set (q := hqlth_between _ _ Hr). apply hinhpr. exists (pr1 q). split. * induction (hqgthorleh 0 (pr1 q)) as [Hq | Hq]. ** exact tt. ** apply fromempty. refine (hqlehtoneghqgth _ _ _ _). *** exact Hq. *** unfold hqlth in q. exact (pr2 (pr2 q)). * exact (pr1 (pr2 q)). + generalize (Hopen _ Dr). apply hinhfun. intros q. exists (pr1 (pr1 q)). induction (hqgthorleh 0 (pr1 (pr1 q))) as [Hq | Hq]. * apply fromempty. refine (hqgthtoneghqleh _ _ _ _). ** apply Hq. ** exact (pr2 (pr1 q)). * split. ** assert (Hq1 : pr1 q = (pr1 (pr1 q) ,, Hq)) by (apply subtypePath_prop ; reflexivity). generalize (pr1 (pr2 q)) ; intro Hq'. rewrite Hq1 in Hq'. exact Hq'. ** generalize (pr2 (pr2 q)) ; intro Hq'. rewrite ltNonnegativeRationals_correct in Hq'. exact Hq'. -intros r q Hrq. induction (hqgthorleh 0 r) as [Hr | Hr]. { apply hinhpr, ii1, tt. } induction (hqgthorleh 0 q) as [Hq | Hq]. + apply fromempty. refine (hqlehtoneghqgth _ _ _ _). * apply Hr. * apply istranshqgth with q. ** exact Hq. ** unfold hqlth in Hrq. exact Hrq. + apply (Dcuts_locatedness (D,,Hbot,,Hopen,,Hcorr)). rewrite ltNonnegativeRationals_correct. exact Hrq. Qed.
Require Import UniMath.RealNumbers.Prelim. Require Import UniMath.RealNumbers.NonnegativeRationals. Require Import UniMath.RealNumbers.NonnegativeReals.