proposition: Lemma Exp_leEq_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_leEq_lft. apply One_leEq_Exp; astepl ( [--]ZeroR); apply inv_resp_leEq; auto. apply less_leEq; apply Exp_pos. Qed.
imports: CoRN.transc.TaylorSeries