Lemma isOneSided_Dcuts_corr : ∏ D, isOneSided D → Dcuts_def_corr (λ r, D (pr1 r)). Proof. intros D H c Hc. rewrite ltNonnegativeRationals_correct in Hc. generalize (pr2 (pr2 H) _ _ Hc). apply hinhuniv ; intros H0. apply coprodcomm in H0. revert H0 ; apply sumofmaps ; intros H0. { apply hinhpr, ii1, H0. } enough (Hq : ∃ q : NonnegativeRationals, D (pr1 q) × ¬ D (pr1 (q + c)%NRat)). { revert Hq. apply hinhfun, ii2. } generalize (pr2 (pr1 H)). apply hinhuniv. intros r. generalize (isarchhq (hqdiv (pr1 r) (hqdiv (pr1 c) 2%hq))). apply hinhuniv. intros n. assert (Hc' : hqdiv (pr1 c) 2 > 0). { apply hqmultgth0gth0. { exact Hc. } apply hqgthandmultlinv with 2. { exact hq2_gt0. } rewrite hqmultx0, hqisrinvmultinv. { exact hq1_gt0. } apply hqgth_hqneq, hq2_gt0. } assert (H1 : hqlth (pr1 r) (nattoring (pr1 n) * (hqdiv (pr1 c) 2))). { unfold hqlth in Hc. apply hqgthandmultrinv with (/ (hqdiv (pr1 c) 2)). - apply hqgthandmultlinv with (hqdiv (pr1 c) 2). + exact Hc'. + rewrite hqmultx0, hqisrinvmultinv. { exact hq1_gt0. } apply hqgth_hqneq, Hc'. - rewrite hqmultassoc, hqisrinvmultinv. + rewrite hqmultr1. unfold hqdiv in n. exact (pr2 n). + apply hqgth_hqneq, Hc'. } assert (Hn : ¬ D (nattoring (pr1 n) * hqdiv (pr1 c) 2)). { generalize (pr2 (pr2 H) _ _ H1). apply (hinhuniv (P := hneg _)), sumofmaps ; intro H2. - apply fromempty, (pr2 r), H2. - apply H2. } assert (H2 : ∏ (m : nat), nattoring m * hqdiv (pr1 c) 2 + pr1 c = nattoring (m + 2) * hqdiv (pr1 c) 2). { intros m. unfold nattoring. rewrite 2!(@nattorig_natmult hq). rewrite natmult_plus. apply maponpaths. simpl. unfold hqdiv. rewrite <- hqmult2r, hqmultassoc. rewrite hqislinvmultinv. - apply pathsinv0, hqmultr1. - apply hqgth_hqneq, hq2_gt0. } generalize (pr1 n) Hn. clear -H H0 Hc Hc' H2 ; intros n Hn. assert (Hm : D (nattoring O * hqdiv (pr1 c) 2)). { rewrite hqmult0x. exact H0. } destruct n. { apply fromempty, Hn, Hm. } rewrite <- (natplusl0 n), plus_n_Sm in Hn. revert Hm Hn. set (m := O). change (D (nattoring m * hqdiv (pr1 c) 2) → ¬ D (nattoring (m + S n) * hqdiv (pr1 c) 2) → ∃ q : NonnegativeRationals, D (pr1 q) × ¬ D (pr1 (q + c)%NRat)). generalize m ; clear m H0. revert D H. induction n as [ | n IHn] ; intros D H m Hm Hn. - apply hinhpr. use tpair. + use tpair. * apply (nattoring m * hqdiv (pr1 c) 2). * abstract (apply hq0lehandmult ; [ clear ; induction m ; [ apply isreflhqleh | unfold nattoring ; rewrite nattorigS ; apply hq0lehandplus ; [ exact hq1ge0 | exact IHm ]] | apply hqlthtoleh, Hc' ]). + simpl. split. * exact Hm. * change (¬ D ((nattoring m * hqdiv (pr1 c) 2) + (pr1 c))). intros H0. refine (factor_through_squash isapropempty _ _). 2: apply (pr2 (pr2 H) (nattoring (m + 1) * hqdiv (pr1 c) 2) (nattoring m * hqdiv (pr1 c) 2 + pr1 c)). ** apply sumofmaps. *** exact Hn. *** intros H1 ; apply H1, H0. ** rewrite H2. apply hqlthandmultr. *** exact Hc'. *** unfold nattoring. rewrite <- (plus_n_Sm m 1%nat). rewrite nattorigS, hqpluscomm. apply hqlthnsn. - refine (hinhuniv _ _). 2: apply (pr2 (pr2 H) (nattoring (m + 1) * hqdiv (pr1 c) 2) (nattoring (m + 2) * hqdiv (pr1 c) 2)). + apply sumofmaps ; intros Hm'. * apply IHn with (m + 1)%nat. ** exact H. ** exact Hm'. ** rewrite natplusassoc. exact Hn. * apply hinhpr. use tpair. ** use tpair. *** apply (nattoring m * hqdiv (pr1 c) 2). *** abstract (apply hq0lehandmult ; [ clear ; induction m ; [ apply isreflhqleh | unfold nattoring ; rewrite nattorigS ; apply hq0lehandplus ; [ exact hq1ge0 | exact IHm ]] | apply hqlthtoleh, Hc' ]). ** simpl. split. *** exact Hm. *** change (¬ D ((nattoring m * hqdiv (pr1 c) 2) + (pr1 c))). rewrite H2. exact Hm'. + apply hqlthandmultr. * exact Hc'. * unfold nattoring. rewrite <- (plus_n_Sm m 1%nat). rewrite nattorigS, hqpluscomm. apply hqlthnsn. Qed.
Require Import UniMath.RealNumbers.Prelim. Require Import UniMath.RealNumbers.NonnegativeRationals. Require Import UniMath.RealNumbers.NonnegativeReals.