proposition: Lemma Taylor_Series_lemma_cont : forall r n, Continuous realline ((r[^]n[/] _[//]nring_fac_ap_zero _ n) {**}f n).
proof: Proof. intros. apply Continuous_scal; case n. apply Continuous_wd with F. apply Derivative_n_unique with H 0 F; auto. apply Derivative_n_O. apply Derivative_n_imp_inc with H n (f n); auto. apply Taylor_Series_imp_cont. clear n; intros. apply Derivative_n_imp_Continuous' with H (S n) F; auto with arith. Qed.
imports: CoRN.transc.PowerSeries CoRN.ftc.Taylor