proposition: Lemma Derivative_Exp : forall H, Derivative realline H Expon Expon.
proof: Proof. intro H. unfold Expon, Exp_ps in |- *. cut (fun_series_convergent_IR realline (FPowerSeries' [0] (fun n : nat => (fun _ : nat => [1]) (S n)))). intro H0. eapply Derivative_wdr. 2: apply Derivative_FPowerSeries1' with (a := fun _ : nat => OneR) (Hg := H0). FEQ. simpl in |- *. apply series_sum_wd; algebra. fold Exp_ps in |- *; apply Exp_conv. Qed.
imports: CoRN.transc.TaylorSeries