Lemma Dcuts_Cauchy_seq_impl_ex_lim_seq (U : nat → Dcuts) (HU : Dcuts_Cauchy_seq U) : is_Dcuts_lim_seq U (Dcuts_lim_cauchy_seq U HU). Proof. intros eps. apply hinhuniv ; intros c'. generalize (is_Dcuts_open _ _ (pr2 (pr2 c'))). apply hinhuniv ; intros c. assert (Hc0 : (0 < pr1 c)%NRat). { eapply istrans_le_lt_ltNonnegativeRationals, (pr2 (pr2 c)). now apply isnonnegative_NonnegativeRationals. } apply ispositive_NQhalf in Hc0. generalize (HU _ (pr2 (isapfun_NonnegativeRationals_to_Dcuts_aux _ _) Hc0)). apply hinhfun ; intros N. exists (pr1 N) ; intros n Hn. generalize (λ n Hn, pr2 N n (pr1 N) Hn (isreflnatleh _)) ; intros Hu. split. - eapply istrans_Dcuts_lt_le_rel. { now apply (Hu n Hn). } pattern eps at 1; rewrite (Dcuts_half_double eps), <- isassoc_Dcuts_plus. eapply istrans_Dcuts_le_rel, Dcuts_plus_lecompat_l. + apply Dcuts_plus_lecompat_r. intros r Hr. simpl. apply is_Dcuts_bot with (1 := pr1 (pr2 c)). rewrite (NQhalf_double (pr1 c)). now apply lt_leNonnegativeRationals, plusNonnegativeRationals_ltcompat ; apply Hr. + intros r Hr. generalize (isdecrel_ltNonnegativeRationals r (pr1 c / 2)%NRat) ; apply sumofmaps ; intro Hrc. * apply hinhpr ; left ; right. apply is_Dcuts_bot with (1 := pr1 (pr2 c)). rewrite (NQhalf_double (pr1 c)). now apply lt_leNonnegativeRationals, plusNonnegativeRationals_ltcompat ; apply Hrc. * apply notlt_geNonnegativeRationals in Hrc. generalize (is_Dcuts_open _ _ Hr). apply hinhuniv ; intros q. apply hinhpr ; right ; exists (r - pr1 c / 2%NRat,, pr1 c / 2%NRat) ; repeat split. ** now simpl ; rewrite minusNonnegativeRationals_plus_r. ** generalize (pr1 q) (pr1 (pr2 q)) (pr2 (pr2 q)) ; clear q ; intros q UNq Hrq. apply hinhpr ; exists (q - r) ; split. { apply ispositive_minusNonnegativeRationals, Hrq. } exists (pr1 N) ; intros m Hm. simpl. rewrite minusNonnegativeRationals_plus_exchange, iscomm_plusNonnegativeRationals, minusNonnegativeRationals_plus_r. *** generalize (Dcuts_lt_le_rel _ _ (pr2 (Hu m Hm)) _ UNq) ; clear Hu. apply hinhuniv ; apply sumofmaps ; [ apply sumofmaps ; [ intros Xr | intros Yr] | intros xy ; rewrite (pr1 (pr2 xy))]. { apply is_Dcuts_bot with (1 := Xr). now apply minusNonnegativeRationals_le. } { simpl in Yr. apply_pr2_in notge_ltNonnegativeRationals Yr. apply fromempty, Yr. apply istrans_leNonnegativeRationals with r. - exact Hrc. - now apply lt_leNonnegativeRationals. } apply is_Dcuts_bot with (1 := pr1 (pr2 (pr2 xy))). apply_pr2 (plusNonnegativeRationals_lecompat_r (pr1 c / 2)%NRat). rewrite minusNonnegativeRationals_plus_r. { apply plusNonnegativeRationals_lecompat_l, lt_leNonnegativeRationals. exact (pr2 (pr2 (pr2 xy))). } apply lt_leNonnegativeRationals. rewrite <- (pr1 (pr2 xy)). eapply istrans_le_lt_ltNonnegativeRationals, Hrq. exact Hrc. *** now apply lt_leNonnegativeRationals. *** exact Hrc. ** simpl ; unfold Dcuts_half_val. rewrite <- NQhalf_double. exact (pr1 (pr2 c)). - apply istrans_Dcuts_le_lt_rel with (Dcuts_plus (U (pr1 N)) (Dcuts_half eps)). + intros r. apply hinhuniv ; intros c''. generalize (isdecrel_ltNonnegativeRationals r (pr1 c / 2)%NRat) ; apply sumofmaps ; intro Hrc. * apply hinhpr ; left ; right. apply is_Dcuts_bot with (1 := pr1 (pr2 c)). rewrite (NQhalf_double (pr1 c)). now apply lt_leNonnegativeRationals, plusNonnegativeRationals_ltcompat ; apply Hrc. * apply notlt_geNonnegativeRationals in Hrc. apply hinhpr ; right ; exists (r - pr1 c / 2%NRat,, pr1 c / 2%NRat) ; simpl ; repeat split. ** now rewrite minusNonnegativeRationals_plus_r. ** generalize (natgthorleh (pr1 N) (pr1 (pr2 (pr2 c'')))) ; apply sumofmaps ; intro HN. { apply natlthtoleh in HN. apply is_Dcuts_bot with (1 := pr2 (pr2 (pr2 c'')) _ HN). apply istrans_leNonnegativeRationals with r. - now apply minusNonnegativeRationals_le. - now apply plusNonnegativeRationals_le_r. } generalize (Dcuts_lt_le_rel _ _ (pr1 (Hu _ HN)) _ (pr2 (pr2 (pr2 c'')) _ (isreflnatleh _))). apply hinhuniv ; apply sumofmaps ; [ apply sumofmaps ; [intros Xr | intros Yr] | intros xy ]. *** apply is_Dcuts_bot with (1 := Xr). apply istrans_leNonnegativeRationals with r. **** now apply minusNonnegativeRationals_le. **** now apply plusNonnegativeRationals_le_r. *** simpl in Yr. apply_pr2_in notge_ltNonnegativeRationals Yr. apply fromempty, Yr. apply istrans_leNonnegativeRationals with r. **** exact Hrc. **** now apply plusNonnegativeRationals_le_r. *** apply is_Dcuts_bot with (1 := pr1 (pr2 (pr2 xy))). apply_pr2 (plusNonnegativeRationals_lecompat_r (pr1 c / 2)%NRat). rewrite minusNonnegativeRationals_plus_r. **** apply istrans_leNonnegativeRationals with (r + pr1 c''). { now apply plusNonnegativeRationals_le_r. } pattern (r + pr1 c'') at 1 ; rewrite (pr1 (pr2 xy)). apply plusNonnegativeRationals_lecompat_l. apply lt_leNonnegativeRationals. exact (pr2 (pr2 (pr2 xy))). **** exact Hrc. ** unfold Dcuts_half_val. rewrite <- NQhalf_double. exact (pr1 (pr2 c)). + pattern eps at 2; rewrite (Dcuts_half_double eps), <- isassoc_Dcuts_plus. apply Dcuts_plus_ltcompat_l. apply istrans_Dcuts_lt_le_rel with (Dcuts_plus (U n) (NonnegativeRationals_to_Dcuts (pr1 c / 2)%NRat)). { now apply (pr2 (Hu _ Hn)). } apply Dcuts_plus_lecompat_r. intros r Hr. apply is_Dcuts_bot with (1 := pr1 (pr2 c)). rewrite (NQhalf_double (pr1 c)). apply lt_leNonnegativeRationals, plusNonnegativeRationals_ltcompat ; apply Hr. 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.