Lemma Cauchy_seq_pr2 (u : nat → hr_ConstructiveField) : let y := λ n : nat, hr_to_NRneg (u n) in Cauchy_seq u → NonnegativeReals.Cauchy_seq y. Proof. intros y. set (x := λ n : nat, hr_to_NRpos (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. } intros Cu c Hc. generalize (Cu c Hc). apply hinhfun ; intros N. exists (pr1 N) ; intros n m Hn Hm. generalize ((pr2 N) _ _ Hn Hm) ; intros Hu. split. - apply (plusNonnegativeReals_ltcompat_r (y m)) in Hu. eapply istrans_le_lt_ltNonnegativeReals, Hu. rewrite hr_opp_minus, hr_abs_opp, ringcomm1. change (- - u n)%ring with (grinv hr_commring (grinv hr_commring (u n))). rewrite (grinvinv hr_commring (u n)). eapply istrans_leNonnegativeReals, plusNonnegativeReals_lecompat_r, maxNonnegativeReals_le_r. eapply istrans_leNonnegativeReals, plusNonnegativeReals_lecompat_r, hr_to_NRneg_minus. change (hr_to_NRneg (u n)) with (y n) ; change (hr_to_NRneg (u m)) with (y m). rewrite iscomm_plusNonnegativeReals, <- maxNonnegativeReals_minus_plus. now apply maxNonnegativeReals_le_l. - apply (plusNonnegativeReals_ltcompat_r (y n)) in Hu. eapply istrans_le_lt_ltNonnegativeReals, Hu. eapply istrans_leNonnegativeReals, plusNonnegativeReals_lecompat_r, maxNonnegativeReals_le_r. eapply istrans_leNonnegativeReals, plusNonnegativeReals_lecompat_r, hr_to_NRneg_minus. change (hr_to_NRneg (u n)) with (y n) ; change (hr_to_NRneg (u m)) with (y m). rewrite iscomm_plusNonnegativeReals, <- maxNonnegativeReals_minus_plus. now apply maxNonnegativeReals_le_l. 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.