proposition: Lemma convergence_lemma : forall r : IR, conv_fun_seq'_IR realline (fun n : nat => [-C-] (r[^]n[/] _[//]nring_fac_ap_zero IR n)) [-C-][0] (fun n : nat => Continuous_const realline _) (Continuous_const realline _).
proof: Proof. red in |- *; intros. apply seq_conv_imp_fun_conv with (x := fun n : nat => r[^]n[/] _[//]nring_fac_ap_zero _ n). clear Hinc Hab b a. apply series_seq_Lim. assert (H : forall n : nat, Dom (Exp_ps n) r). repeat split. apply convergent_wd with (fun n : nat => Part (Exp_ps n) r (H n)). Opaque nexp_op. intros; simpl in |- *. rstepl ((r[-][0]) [^]n[/] _[//]nring_fac_ap_zero _ n). algebra. apply fun_series_conv_imp_conv_IR with realline. apply Exp_conv. split. Qed.
imports: CoRN.transc.PowerSeries CoRN.ftc.Taylor