proposition: Lemma insert_series_cont : forall n, Continuous J (insert_series n).
proof: Proof. intro; elim n; intros. simpl in |- *; apply Continuous_const. simpl in |- *; apply convergent_imp_Continuous; auto. Qed.
imports: CoRN.ftc.FunctSeries CoRN.ftc.MoreFunctions