proposition: Lemma Exp_plus_pos : forall z, [0] [<] z -> forall x, Exp (x[+]z) [=] Exp x[*]Exp z.
proof: Proof. intros z H x. set (F := ([1][/] _[//]pos_ap_zero _ _ (Exp_pos' _ H)) {**} (Expon[o]FId{+}[-C-]z)) in *. apply eq_symmetric_unfolded. rstepr ((Exp (x[+]z) [/] _[//]pos_ap_zero _ _ (Exp_pos' _ H)) [*]Exp z). apply mult_wdl. unfold Exp at 1 in |- *. simpl in |- *. assert (H0 : Dom F x). repeat split; exists (I, I); apply Exp_domain. apply eq_transitive_unfolded with (Part F x H0). 2: unfold F, Exp in |- *; simpl in |- *; rational. apply Feq_imp_eq with realline. apply Exp_unique. assert (H1 : Derivative realline I Expon Expon). apply Derivative_Exp. unfold F in |- *; Derivative_Help. apply eq_imp_Feq. apply included_FScalMult; apply included_FMult. apply included_FComp; Included. Included. apply included_FScalMult; apply included_FComp; Included. intros; simpl in |- *; rational. apply Derivative_scal. apply Derivative_comp with realline I; Deriv. red in |- *; intros a b Hab H2. exists (a[+]z); exists (b[+]z[+][1]). cut (a[+]z [<] b[+]z[+][1]). intro H3. exists H3; repeat split; simpl in |- *; try rename H4 into X; elim X; try intros H5 H6. apply plus_resp_leEq; auto. apply leEq_transitive with (b[+]z). apply plus_resp_leEq; auto. apply less_leEq; apply less_plusOne. apply leEq_less_trans with (b[+]z). apply plus_resp_leEq; auto. apply less_plusOne. intro H1; simpl in |- *. rational. split. Qed.
imports: CoRN.transc.TaylorSeries