proposition: Lemma Exp_resp_less : forall x y : IR, x [<] y -> Exp x [<] Exp y.
proof: Proof. intros x y H. apply less_wdr with (Exp (x[+] (y[-]x))). 2: apply Exp_wd; rational. astepr (Exp x[*]Exp (y[-]x)). astepl (Exp x[*][1]). apply mult_resp_less_lft. apply One_less_Exp. apply shift_less_minus; astepl x; auto. apply Exp_pos. Qed.
imports: CoRN.transc.TaylorSeries