proposition: Lemma derivable_pt_lim_Cpow : forall (z : C) (n:nat), derivable_pt_lim (fun z => z ^ (S n)) z (INC (S n) * z ^ n).
proof: Proof. intros z n ; induction n. simpl ; rewrite Cmult_1_r ; intros eps eps_pos. exists (mkposreal 1 Rlt_0_1) ; intros ; apply Rle_lt_trans with (Cnorm C0). right ; apply Cnorm_eq_compat. field; auto. rewrite Cnorm_C0. assumption. replace (fun z0 : C => z0 ^ S (S n)) with (fun z0 : C => z0 * (z0 ^ (S n))). replace (INC (S (S n)) * z ^ S n) with ((1 * (z ^ (S n))) + z * ((INC (S n) * z ^ n))). assert (H' := derivable_pt_lim_id z). assert (Main := derivable_pt_lim_mult id (fun z => Cpow z (S n)) z 1 (INC (S n) * z ^ n) H' IHn). apply Main. rewrite Cmult_1_l ; simpl ; ring. reflexivity. Qed.
imports: Cprop_base Ctacfield Cfunctions Cpow Csequence_def Cpser_def Cpser_base_facts Canalysis_def Canalysis_deriv