proposition: Lemma Exp_plus : forall x y : IR, Exp (x[+]y) [=] Exp x[*]Exp y.
proof: Proof. intros x y. set (z := Max [1] ([1][-]y)) in *. cut ([0] [<] z). intro H. apply mult_cancel_rht with (Exp z). apply Greater_imp_ap; apply Exp_pos'; auto. eapply eq_transitive_unfolded. apply eq_symmetric_unfolded; apply Exp_plus_pos; auto. astepl (Exp (x[+] (y[+]z))). eapply eq_transitive_unfolded. apply Exp_plus_pos. 2: astepr (Exp x[*] (Exp y[*]Exp z)); apply mult_wdr; apply Exp_plus_pos; auto. unfold z in |- *. apply shift_less_plus'; astepl ( [--]y). apply less_leEq_trans with ([1][-]y). eapply less_wdr. apply less_plusOne. rational. apply rht_leEq_Max. apply less_leEq_trans with OneR. apply pos_one. unfold z in |- *; apply lft_leEq_Max. Qed.
imports: CoRN.transc.TaylorSeries