proposition: Lemma Exp_one : Exp [1] [=] E.
proof: Proof. unfold E, Exp, e_series in |- *; simpl in |- *. apply series_sum_wd; intro n. astepr (([1][/] _[//]nring_fac_ap_zero IR n) [*][1]); apply mult_wdr. astepl (([1][+][--]ZeroR) [^]n). eapply eq_transitive_unfolded. 2: apply (one_nexp IR n). apply nexp_wd; rational. Qed.
imports: CoRN.transc.TaylorSeries