Lemma Cauchy_seq_impl_ex_lim_seq (u : nat → hr_ConstructiveField) : Cauchy_seq u → ex_lim_seq u. Proof. intros Cu. set (x := λ n, hr_to_NRpos (u n)). set (y := λ n, hr_to_NRneg (u n)). assert (Hxy : ∏ n, NR_to_hr (x n ,, y n) = u n). { intros n. unfold x, y, hr_to_NRpos, hr_to_NRneg. apply hr_to_NR_bij. } generalize (Cauchy_seq_impl_ex_lim_seq x (Cauchy_seq_pr1 u Cu)). set (lx := Cauchy_lim_seq x (Cauchy_seq_pr1 u Cu)) ; clearbody lx ; intro Hx. generalize (Cauchy_seq_impl_ex_lim_seq y (Cauchy_seq_pr2 u Cu)). set (ly := Cauchy_lim_seq y (Cauchy_seq_pr2 u Cu)) ; clearbody ly ; intro Hy. exists (NR_to_hr (lx,,ly)). intros c Hc. apply ispositive_halfNonnegativeReals in Hc. generalize (Hx _ Hc) (Hy _ Hc) ; apply hinhfun2 ; clear Hy Hx ; intros Nx Ny. exists (max (pr1 Nx) (pr1 Ny)) ; intros n Hn. rewrite <- Hxy ; simpl pr1. rewrite NR_to_hr_minus ; simpl. apply maxNonnegativeReals_lt. - rewrite hr_to_NRpos_NR_to_hr. apply_pr2 (plusNonnegativeReals_ltcompat_r (y n + lx)). rewrite iscomm_plusNonnegativeReals, <- maxNonnegativeReals_minus_plus ; simpl. apply maxNonnegativeReals_lt. + rewrite (double_halfNonnegativeReals c), (iscomm_plusNonnegativeReals (y n)), (isassoc_plusNonnegativeReals lx (y n)), <- (isassoc_plusNonnegativeReals (y n)), (iscomm_plusNonnegativeReals (y n)), <- !isassoc_plusNonnegativeReals, (isassoc_plusNonnegativeReals (lx + _)). apply plusNonnegativeReals_ltcompat. * apply (pr2 Nx). apply istransnatleh with (2 := Hn). apply max_le_l. * apply_pr2 (pr2 Ny). apply istransnatleh with (2 := Hn). apply max_le_r. + apply plusNonnegativeReals_lt_r . now apply_pr2 ispositive_halfNonnegativeReals. - rewrite hr_to_NRneg_NR_to_hr. apply_pr2 (plusNonnegativeReals_ltcompat_r (x n + ly)). rewrite iscomm_plusNonnegativeReals, <- maxNonnegativeReals_minus_plus ; simpl. apply maxNonnegativeReals_lt. + rewrite (double_halfNonnegativeReals c), (iscomm_plusNonnegativeReals (x n)), (isassoc_plusNonnegativeReals ly (x n)), <- (isassoc_plusNonnegativeReals (x n)), (iscomm_plusNonnegativeReals (x n)), <- !isassoc_plusNonnegativeReals, (isassoc_plusNonnegativeReals (ly + _)). apply plusNonnegativeReals_ltcompat. * apply (pr2 Ny). apply istransnatleh with (2 := Hn). apply max_le_r. * apply_pr2 (pr2 Nx). apply istransnatleh with (2 := Hn). apply max_le_l. + apply plusNonnegativeReals_lt_r . now apply_pr2 ispositive_halfNonnegativeReals. Qed.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.RealNumbers.Prelim. Require Import UniMath.RealNumbers.Sets. Require Import UniMath.RealNumbers.NonnegativeRationals.