proposition: Lemma Cauchy_equiv : Cauchy_crit Un <-> (Rseries.Cauchy_crit (fun n => Cre (Un n)) /\ Rseries.Cauchy_crit (fun n => Cim (Un n)))%R.
proof: Proof. split. intro Un_cauchy ; split ; intros eps eps_pos ; destruct (Un_cauchy eps eps_pos) as [N HN] ; exists N ; intros m n m_lb n_lb. apply Rle_lt_trans with (Cnorm (Cre (Un m - Un n))%C)%R ; [right |]. unfold R_dist ; rewrite Cnorm_IRC_Rabs ; apply Rabs_eq_compat ; apply Cre_minus_compat. rewrite Cnorm_IRC_Rabs ; apply Rle_lt_trans with (Cnorm (Un m - Un n))%R ; [apply Cre_le_Cnorm | apply HN] ; assumption. apply Rle_lt_trans with (Cnorm (Cim (Un m - Un n))%C)%R ; [right |]. unfold R_dist ; rewrite Cnorm_IRC_Rabs ; apply Rabs_eq_compat ; apply Cim_minus_compat. rewrite Cnorm_IRC_Rabs ; apply Rle_lt_trans with (Cnorm (Un m - Un n))%R ; [apply Cim_le_Cnorm | apply HN] ; assumption. intros [Cre_cauchy Cim_cauchy] ; intros eps eps_pos ; assert (eps_2_pos : 0 < eps / 2) by lra ; destruct (Cre_cauchy (eps / 2)%R eps_2_pos) as [N1 HN1] ; destruct (Cim_cauchy (eps / 2)%R eps_2_pos) as [N2 HN2] ; unfold R_dist in * ; exists (Nat.max N1 N2) ; intros m n m_ub n_ub. apply Rle_lt_trans with (Rabs (Cre (Un m - Un n)) + Rabs (Cim (Un m - Un n)))%R ; [apply Cnorm_le_Cre_Cim | apply Rlt_le_trans with (eps / 2 + eps / 2)%R ; [| right ; field]]. apply Rlt_trans with (Rabs (Cre (Un m - Un n)) + eps / 2)%R. apply Rplus_lt_compat_l ; rewrite <- Cim_minus_compat ; apply HN2 ; apply Nat.le_trans with (Nat.max N1 N2) ; [apply Nat.le_max_r | assumption | apply Nat.le_max_r | assumption]. apply Rplus_lt_compat_r. rewrite <- Cre_minus_compat ; apply HN1 ; apply Nat.le_trans with (Nat.max N1 N2) ; [apply Nat.le_max_l | assumption | apply Nat.le_max_l | assumption]. Qed.
imports: MyReals PeanoNat Rsequence_def Rsequence_facts Rsequence_base_facts Lia Lra Complex Csequence_def