proposition: Lemma Cpser_alembert_prelim2 : forall (An : nat -> C) (M : R), 0 < M -> (forall n : nat, An n <> C0) -> Cseq_eventually (fun Un => Cseq_bound Un M) (fun n => (An (S n) / An n)) -> forall r, Rabs r < / M -> Cv_radius_weak An r.
proof: Proof. intros An M M_pos An_neq An_frac_event r r_bd. destruct An_frac_event as [N HN]. assert (Rho : Cv_radius_weak (fun n => (An (N + n)%nat)) r). apply Cpser_alembert_prelim with M. assumption. intro n ; apply An_neq. intro n ; replace (N + S n)%nat with (S (N + n)) by intuition ; apply HN. assumption. apply Cv_radius_weak_padding_neg_compat with N ; destruct Rho as [T HT] ; exists T ; intros u Hu ; destruct Hu as [n Hn] ; rewrite Hn ; unfold_gt ; rewrite Nat.add_comm ; apply HT ; exists n ; reflexivity. 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