proposition: Lemma Cpser_alembert_prelim4 : forall (An : nat -> C), (forall n : nat, An n <> C0) -> Rseq_cv (fun n : nat => Cnorm (An (S n) / An n)) R0 -> infinite_cv_radius An.
proof: Proof. intros An An_neq An_frac_0 r. assert (eps_pos : 0 < /(Rabs r + 1)). apply Rinv_0_lt_compat ; apply Rplus_le_lt_0_compat ; [apply Rabs_pos | apply Rlt_0_1]. apply Cpser_alembert_prelim2 with (/(Rabs r + 1))%R. assumption. apply An_neq. destruct (An_frac_0 (/ (Rabs r + 1))%R eps_pos) as [N HN] ; exists N ; intro n. apply Rle_trans with (R_dist (Cnorm (An (S (N + n)) / An (N + n)%nat)) 0) ; [right |]. unfold R_dist in |-* ; rewrite Rminus_0_r, Rabs_right ; [reflexivity | apply Rle_ge ; apply Cnorm_pos]. left ; apply HN ; intuition. rewrite Rinv_involutive ; [lra |] ; apply Rgt_not_eq ; apply Rplus_le_lt_0_compat ; [apply Rabs_pos | apply Rlt_0_1]. Qed.
imports: Rinterval Ranalysis_def Rpser_def Rpser_base_facts Rpser_cv_facts Rpser_sums Rpow_facts Rsequence_def Rsequence_facts Rseries_def Rseries_facts RFsequence_facts Cpow Cpser_def Cpser_base_facts CFsequence CFsequence_facts Csequence Csequence_def Csequence_facts Cmet Cnorm Ctacfield Cprop_base Canalysis_def Canalysis_cont Canalysis_deriv Canalysis_basic_facts