Lemma Dcuts_lim_cauchy_corr : Dcuts_def_corr Dcuts_lim_cauchy_val. Proof. intros c Hc. apply ispositive_NQhalf, ispositive_NQhalf in Hc. generalize (U_cauchy _ Hc) ; clear U_cauchy ; apply hinhuniv ; intros N. generalize (λ n Hn, pr2 N n (pr1 N) Hn (isreflnatleh _)) ; intro Hu. generalize (U_corr (pr1 N) _ Hc). apply hinhuniv ; apply sumofmaps ; intros HuN. - apply hinhpr ; left. intro ; apply HuN ; clear HuN. revert X ; apply hinhuniv ; intros eps. generalize (natgthorleh (pr1 N) (pr1 (pr2 (pr2 eps)))) ; apply sumofmaps ; intros HN. + apply natlthtoleh in HN. apply (U_bot (pr1 N)) with (1 := pr2 (pr2 (pr2 eps)) _ HN). pattern c at 2 ; rewrite (NQhalf_double c), isassoc_plusNonnegativeRationals. pattern (c / 2)%NRat at 2 ; rewrite (NQhalf_double (c / 2)%NRat), isassoc_plusNonnegativeRationals. now apply plusNonnegativeRationals_le_r. + generalize (pr2 (pr2 (pr2 eps)) _ (isreflnatleh _)) ; intros HuN'. generalize (pr1 (Hu _ HN) _ HuN') ; clear Hu HuN'. apply hinhuniv ; apply sumofmaps ; [ apply sumofmaps ; intros H | intros xy ]. * apply (U_bot (pr1 N)) with (1 := H). pattern c at 2 ; rewrite (NQhalf_double c), isassoc_plusNonnegativeRationals. pattern (c / 2)%NRat at 2 ; rewrite (NQhalf_double (c / 2)%NRat), isassoc_plusNonnegativeRationals. now apply plusNonnegativeRationals_le_r. * apply fromempty. revert H. apply_pr2 notlt_geNonnegativeRationals. pattern c at 2 ; rewrite (NQhalf_double c), isassoc_plusNonnegativeRationals. pattern (c / 2)%NRat at 2 ; rewrite (NQhalf_double (c / 2)%NRat), isassoc_plusNonnegativeRationals. now apply plusNonnegativeRationals_le_r. * apply (U_bot (pr1 N)) with (1 := pr1 (pr2 (pr2 xy))). apply_pr2 (plusNonnegativeRationals_lecompat_r (pr2 (pr1 xy))). rewrite <- (pr1 (pr2 xy)). pattern c at 2; rewrite (NQhalf_double c), isassoc_plusNonnegativeRationals. pattern (c / 2)%NRat at 2; rewrite (NQhalf_double (c / 2)%NRat), isassoc_plusNonnegativeRationals. apply plusNonnegativeRationals_lecompat_l. apply istrans_leNonnegativeRationals with (c / 2 / 2)%NRat. ** apply lt_leNonnegativeRationals. exact (pr2 (pr2 (pr2 xy))). ** now apply plusNonnegativeRationals_le_r. - rename HuN into q. generalize (isdecrel_leNonnegativeRationals (pr1 q) (c / 2)%NRat) ; apply sumofmaps ; intros Hq. + apply hinhpr ; left. intro ; apply (pr2 (pr2 q)). revert X ; apply hinhuniv ; intros eps. generalize (natgthorleh (pr1 N) (pr1 (pr2 (pr2 eps)))) ; apply sumofmaps ; intros HN. * apply natlthtoleh in HN. apply (U_bot (pr1 N)) with (1 := pr2 (pr2 (pr2 eps)) _ HN). pattern c at 2; rewrite (NQhalf_double c), isassoc_plusNonnegativeRationals. apply istrans_leNonnegativeRationals with (c / 2 + c / 2 / 2)%NRat. ** apply plusNonnegativeRationals_lecompat_r. exact Hq. ** apply plusNonnegativeRationals_lecompat_l. pattern (c / 2)%NRat at 2 ; rewrite (NQhalf_double (c / 2)%NRat), isassoc_plusNonnegativeRationals. now apply plusNonnegativeRationals_le_r. * generalize (pr2 (pr2 (pr2 eps)) _ (isreflnatleh _)) ; intros HuN'. generalize (pr1 (Hu _ HN) _ HuN') ; clear Hu HuN'. apply hinhuniv ; apply sumofmaps ; [ apply sumofmaps ; intros H | intros xy]. { apply (U_bot (pr1 N)) with (1 := H). pattern c at 2; rewrite (NQhalf_double c), isassoc_plusNonnegativeRationals, iscomm_plusNonnegativeRationals. apply istrans_leNonnegativeRationals with (c / 2 / 2 + c / 2)%NRat. ** apply plusNonnegativeRationals_lecompat_l. exact Hq. ** rewrite iscomm_plusNonnegativeRationals. apply plusNonnegativeRationals_lecompat_l. pattern (c / 2)%NRat at 2 ; rewrite (NQhalf_double (c / 2)%NRat), isassoc_plusNonnegativeRationals. now apply plusNonnegativeRationals_le_r. } { apply fromempty. revert H. apply_pr2 notlt_geNonnegativeRationals. pattern c at 2 ; rewrite (NQhalf_double c), isassoc_plusNonnegativeRationals. pattern (c / 2)%NRat at 2 ; rewrite (NQhalf_double (c / 2)%NRat), isassoc_plusNonnegativeRationals. now apply plusNonnegativeRationals_le_r. } { apply (U_bot (pr1 N)) with (1 := pr1 (pr2 (pr2 xy))). apply_pr2 (plusNonnegativeRationals_lecompat_r (pr2 (pr1 xy))). rewrite <- (pr1 (pr2 xy)). pattern c at 2; rewrite (NQhalf_double c), !isassoc_plusNonnegativeRationals. eapply istrans_leNonnegativeRationals. - apply plusNonnegativeRationals_lecompat_r. now apply Hq. - apply plusNonnegativeRationals_lecompat_l. pattern (c / 2)%NRat at 2; rewrite (NQhalf_double (c / 2)%NRat), isassoc_plusNonnegativeRationals. apply plusNonnegativeRationals_lecompat_l. apply istrans_leNonnegativeRationals with (c / 2 / 2)%NRat. + apply lt_leNonnegativeRationals. exact (pr2 (pr2 (pr2 xy))). + now apply plusNonnegativeRationals_le_r. } + apply hinhpr ; right. apply notge_ltNonnegativeRationals in Hq. exists (pr1 q - c / 2)%NRat ; split. * apply hinhpr. exists (c / 2 / 2)%NRat ; split. ** exact Hc. ** exists (pr1 N) ; intros n Hn. generalize (pr2 (Hu _ Hn) _ (pr1 (pr2 q))). apply hinhuniv ; apply sumofmaps ; [ apply sumofmaps ; [intros Xr | intros Yr] | intros xy]. { apply (U_bot n) with (1 := Xr). pattern (pr1 q) at 2 ; rewrite <- (minusNonnegativeRationals_plus_r (c / 2)%NRat (pr1 q)). - apply plusNonnegativeRationals_lecompat_l. pattern (c / 2)%NRat at 2 ; rewrite (NQhalf_double (c / 2)%NRat). now apply plusNonnegativeRationals_le_r. - now apply lt_leNonnegativeRationals. } { apply fromempty. revert Yr. apply_pr2 notlt_geNonnegativeRationals. eapply istrans_leNonnegativeRationals, lt_leNonnegativeRationals, Hq. pattern (c / 2)%NRat at 2 ; rewrite (NQhalf_double (c / 2)%NRat). now apply plusNonnegativeRationals_le_r. } { apply (U_bot n) with (1 := pr1 (pr2 (pr2 xy))). apply_pr2 (plusNonnegativeRationals_lecompat_r (pr2 (pr1 xy))). rewrite <- (pr1 (pr2 xy)). pattern (pr1 q) at 2; rewrite <- (minusNonnegativeRationals_plus_r (c / 2)%NRat (pr1 q)), isassoc_plusNonnegativeRationals. - apply plusNonnegativeRationals_lecompat_l. pattern (c / 2)%NRat at 2; rewrite (NQhalf_double (c / 2)%NRat). apply plusNonnegativeRationals_lecompat_l. apply lt_leNonnegativeRationals. exact (pr2 (pr2 (pr2 xy))). - now apply lt_leNonnegativeRationals. } * intro ; apply (pr2 (pr2 q)). revert X ; apply hinhuniv ; intros eps. generalize (natgthorleh (pr1 N) (pr1 (pr2 (pr2 eps)))) ; apply sumofmaps ; intros HN. { apply natlthtoleh in HN. apply (U_bot (pr1 N)) with (1 := pr2 (pr2 (pr2 eps)) _ HN). pattern c at 3; rewrite (NQhalf_double c), <- isassoc_plusNonnegativeRationals, minusNonnegativeRationals_plus_r. - pattern (c / 2)%NRat at 2; rewrite (NQhalf_double (c / 2)%NRat), !isassoc_plusNonnegativeRationals, <- (isassoc_plusNonnegativeRationals (pr1 q) (c / 2 / 2)%NRat). now apply plusNonnegativeRationals_le_r. - now apply lt_leNonnegativeRationals. } { generalize (pr2 (pr2 (pr2 eps)) _ (isreflnatleh _)) ; intros HuN. generalize (pr1 (Hu _ HN) _ HuN) ; clear Hu HuN. apply hinhuniv ; apply sumofmaps ; [ apply sumofmaps ; intros H | intros xy]. - apply (U_bot (pr1 N)) with (1 := H). pattern (pr1 q) at 1 ; rewrite <- (minusNonnegativeRationals_plus_r (c / 2)%NRat (pr1 q)), !isassoc_plusNonnegativeRationals. + apply plusNonnegativeRationals_lecompat_l. pattern c at 3 ; rewrite (NQhalf_double c), isassoc_plusNonnegativeRationals. apply plusNonnegativeRationals_lecompat_l. pattern (c / 2)%NRat at 2 ; rewrite (NQhalf_double (c / 2)%NRat), isassoc_plusNonnegativeRationals. now apply plusNonnegativeRationals_le_r. + now apply lt_leNonnegativeRationals. - apply fromempty. revert H. apply_pr2 notlt_geNonnegativeRationals. eapply istrans_leNonnegativeRationals, plusNonnegativeRationals_le_r. eapply istrans_leNonnegativeRationals, plusNonnegativeRationals_le_l. pattern c at 2 ; rewrite (NQhalf_double c). pattern (c / 2)%NRat at 2 ; rewrite (NQhalf_double (c / 2)%NRat), isassoc_plusNonnegativeRationals. now apply plusNonnegativeRationals_le_r. - apply (U_bot (pr1 N)) with (1 := pr1 (pr2 (pr2 xy))). apply_pr2 (plusNonnegativeRationals_lecompat_r (pr2 (pr1 xy))). rewrite <- (pr1 (pr2 xy)). pattern (pr1 q) at 1 ; rewrite <- (minusNonnegativeRationals_plus_r (c / 2)%NRat (pr1 q)), !isassoc_plusNonnegativeRationals. + pattern (pr1 q - c / 2 + c + pr1 eps)%NRat; rewrite (isassoc_plusNonnegativeRationals (pr1 q - c / 2)%NRat c (pr1 eps)). apply plusNonnegativeRationals_lecompat_l. pattern c at 3; rewrite (NQhalf_double c). pattern (c / 2 + c / 2 + pr1 eps)%NRat at 1 ; rewrite isassoc_plusNonnegativeRationals. apply plusNonnegativeRationals_lecompat_l. pattern (c / 2)%NRat at 2; rewrite (NQhalf_double (c / 2)%NRat). pattern (c / 2 / 2 + c / 2 / 2 + pr1 eps)%NRat at 1 ; rewrite isassoc_plusNonnegativeRationals. apply plusNonnegativeRationals_lecompat_l. apply istrans_leNonnegativeRationals with (c / 2 / 2)%NRat. * apply lt_leNonnegativeRationals. exact (pr2 (pr2 (pr2 xy))). * now apply plusNonnegativeRationals_le_r. + now apply lt_leNonnegativeRationals. } 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.