proposition: Lemma ex_lim_seq_cauchy_corr (u : nat -> R) : (ex_finite_lim_seq u) <-> ex_lim_seq_cauchy u.
proof: Proof. split => Hcv. apply Lim_seq_correct' in Hcv. apply is_lim_seq_spec in Hcv. move => eps. case: (Hcv (pos_div_2 eps)) => /= {Hcv} N H. exists N => n m Hn Hm. replace (u n - u m) with ((u n - (real (Lim_seq u))) - (u m - (real (Lim_seq u)))) by ring. apply Rle_lt_trans with (1 := Rabs_triang _ _). rewrite Rabs_Ropp (double_var eps). apply Rplus_lt_compat ; by apply H. exists (LimSup_seq u). apply is_lim_seq_spec. intros eps. rewrite /LimSup_seq ; case: ex_LimSup_seq => /= l Hl. case: (Hcv (pos_div_2 eps)) => {Hcv} /= Ncv Hcv. case: l Hl => [l | | ] /= Hl. case: (Hl (pos_div_2 eps)) => {Hl} /= H1 [Nl H2]. exists (Ncv + Nl)%nat => n Hn. apply Rabs_lt_between' ; split. case: (H1 Ncv) => {H1} m [Hm H1]. replace (l - eps) with ((l - eps / 2) - eps / 2) by field. apply Rlt_trans with (u m - eps / 2). by apply Rplus_lt_compat_r. apply Rabs_lt_between'. apply Hcv ; intuition. apply Rlt_trans with (l + eps / 2). apply H2 ; intuition. apply Rminus_lt_0 ; field_simplify ; rewrite ?Rdiv_1. by apply is_pos_div_2. move: (fun n Hn => proj2 (proj1 (Rabs_lt_between' _ _ _) (Hcv n Ncv Hn (Nat.le_refl _)))) => {} Hcv. case: (Hl (u Ncv + eps / 2) Ncv) => {Hl} n [Hn Hl]. contradict Hl ; apply Rle_not_lt, Rlt_le. by apply Hcv. move: (fun n Hn => proj1 (proj1 (Rabs_lt_between' _ _ _) (Hcv n Ncv Hn (Nat.le_refl _)))) => {} Hcv. case: (Hl (u Ncv - eps / 2)) => {Hl} N Hl. move: (Hcv _ (Nat.le_add_r Ncv N)) => H. contradict H ; apply Rle_not_lt, Rlt_le, Hl, MyNat.le_add_l. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy