proposition: Lemma derivable_pt_lim_sum (f : nat -> R -> R) (x : R) (lf : nat -> R) : (forall i, (i <= n)%nat -> derivable_pt_lim (f i) x (lf i)) -> derivable_pt_lim (fun y => (sum_f_R0 (fun n => f n y) n)) x (sum_f_R0 lf n).
proof: Proof. elim n. intros Hf; simpl; apply derivable_pt_lim_eq with (f O); trivial. now apply (Hf 0%nat). intros n' IHn Hf; simpl; apply derivable_pt_lim_plus. now apply IHn; intros i Hi; apply Hf; auto. now apply Hf. Qed.
imports: Coq(Reals Psatz) Coquelicot(Coquelicot) Stdlib