proposition: Lemma One_less_Exp : forall x : IR, [0] [<] x -> [1] [<] Exp x.
proof: Proof. unfold Exp in |- *; simpl in |- *; intros x H. unfold series_sum in |- *. apply less_leEq_trans with ([1][+]x). astepl (OneR[+][0]); apply plus_resp_less_lft; auto. apply str_leEq_seq_so_leEq_Lim. exists 2; intros i Hi. simpl in |- *. unfold seq_part_sum in |- *. induction i as [| i Hreci]. exfalso; inversion Hi. clear Hreci. induction i as [| i Hreci]. exfalso; inversion Hi; inversion H1. clear Hreci. induction i as [| i Hreci]. simpl in |- *. apply eq_imp_leEq; rational. eapply leEq_transitive. apply Hreci; auto with arith. clear Hreci. eapply leEq_wdl. 2: apply cm_rht_unit_unfolded. set (j := S (S i)) in *; clearbody j. simpl in |- *; apply plus_resp_leEq_lft. apply less_leEq; apply mult_resp_pos. apply recip_resp_pos; apply pos_nring_fac. astepr ((x[+][--][0]) [^]j); apply nexp_resp_pos. rstepr x; auto. Qed.
imports: CoRN.transc.TaylorSeries