proposition: Lemma Exp_minus : forall x y : IR, Exp (x[-]y) [=] (Exp x[/] _[//]Exp_ap_zero y).
proof: Proof. intros x y. unfold cg_minus in |- *; astepl (Exp x[*]Exp [--]y). rstepr (Exp x[*] ([1][/] _[//]Exp_ap_zero y)). algebra. Qed.
imports: CoRN.transc.TaylorSeries