proposition: Lemma derivable_sum_f_C0 : forall (An : nat -> C -> C), (forall n, derivable (An n)) -> forall n, derivable (fun z => sum_f_C0 (fun n => An n z) n).
proof: Proof. intros An An_deriv n ; induction n. simpl ; apply An_deriv. simpl ; apply derivable_add ; [apply IHn | apply An_deriv]. Qed.
imports: Cprop_base Ctacfield Cfunctions Cpow Csequence_def Cpser_def Cpser_base_facts Canalysis_def Canalysis_deriv