proposition: Lemma Exp_less_One : forall x : IR, x [<] [0] -> Exp x [<] [1].
proof: Proof. intros x H. astepr (Exp x[*]Exp [--]x). astepl (Exp x[*][1]). apply mult_resp_less_lft. apply One_less_Exp; astepl ( [--]ZeroR); apply inv_resp_less; auto. apply Exp_pos. Qed.
imports: CoRN.transc.TaylorSeries