proposition: Lemma Exp_zero : Exp [0] [=] [1].
proof: Proof. unfold Exp in |- *; simpl in |- *. set (h := (fun n : nat => match n with | O => [1] | S p => [0] end):nat -> IR) in *. cut (forall n : nat, h n [=] ([1][/] _[//]nring_fac_ap_zero _ n) [*]nexp _ n ([0][-][0])). intro H. cut (convergent h). intro H0. apply eq_transitive_unfolded with (series_sum h H0). apply series_sum_wd; algebra. unfold series_sum in |- *. apply eq_symmetric_unfolded. eapply eq_transitive_unfolded. apply Lim_const. apply Lim_seq_eq_Lim_subseq with (f := fun n : nat => S n). auto with arith. intro n; exists (S n); split; auto with arith. intro n; simpl in |- *. induction n as [| n Hrecn]; simpl in |- *; [ algebra | Step_final (OneR[+][0]) ]. apply convergent_wd with (fun n : nat => ([1][/] _[//]nring_fac_ap_zero IR n) [*]nexp _ n ([0][-][0])). algebra. exact (fun_series_conv_imp_conv [0] [0] (leEq_reflexive IR [0]) Exp_ps (Exp_conv [0] [0] (leEq_reflexive IR [0]) (compact_single_iprop realline [0] I)) [0] (compact_single_prop [0]) (fun_series_inc_IR realline Exp_ps Exp_conv [0] I)). simple destruct n; simpl in |- *; intros; rational. Qed.
imports: CoRN.transc.TaylorSeries