proposition: Lemma continuity_pt_sum (f : nat -> R -> R) (x : R) : (forall k, (k <= n)%nat -> continuity_pt (f k) x) -> continuity_pt (fun y => (sum_f_R0 (fun n => f n y) n)) x.
proof: Proof. elim n. now intro Hf; simpl; apply continuity_pt_ext with (f O); trivial; apply Hf. intros n' IHn Hf; simpl; apply continuity_pt_plus. apply IHn; intros k Hk; apply Hf; lia. now apply Hf. Qed.
imports: Coq(Reals Psatz) Coquelicot(Coquelicot) Stdlib