proposition: Lemma derivable_pt_lim_gt_pser : forall An z n, derivable_pt_lim (fun x : C => gt_pser An x (S n)) z (gt_pser (An_deriv An) z n).
proof: Proof. intros An z n ; unfold An_deriv, gt_pser, Cseq_mult, Cseq_shift ; induction n. simpl ; intros eps eps_pos ; exists (mkposreal 1 Rlt_0_1) ; intros ; apply Rle_lt_trans with (Cnorm C0) ; [right ; apply Cnorm_eq_compat ; field | rewrite Cnorm_C0] ; assumption. assert (Main := derivable_pt_lim_mult (fun _ => An (S (S n))) (fun z => Cpow z (S (S n))) z 0 (INC (S (S n)) * z ^ (S n)) (derivable_pt_lim_const _ _) (derivable_pt_lim_Cpow _ _)). rewrite Cmult_0_l, Cadd_0_l in Main. replace (INC (S (S n)) * An (S (S n)) * z ^ S n) with (An (S (S n)) * (INC (S (S n)) * z ^ S n)) by ring. assumption. Qed.
imports: Cprop_base Ctacfield Cfunctions Cpow Csequence_def Cpser_def Cpser_base_facts Canalysis_def Canalysis_deriv