proposition: Lemma Exp_pos : forall x : IR, [0] [<] Exp x.
proof: Proof. intro x. cut (Exp x[*]Exp [--]x [=] [1]); [ intro | apply Exp_inv_char ]. cut ( [--][1] [<=] OneR). intro H0. cut (Continuous_I H0 Expon). intro H1. elim H1; intros Hinc contExp. elim (contExp _ (pos_half IR)); clear H1 Hinc contExp; intros d H1 H2. cut ([0] [<] Min d [1]); [ intro H3 | apply less_Min; auto; apply pos_one ]. cut ( [--] (Min d [1]) [<] [0]); [ intro H4 | astepr ( [--]ZeroR); apply inv_resp_less; auto ]. elim (less_cotransitive _ _ _ H4 x); intro H5. elim (less_cotransitive _ _ _ H3 x); intro H6. apply Exp_pos'; auto. apply less_leEq_trans with (Half:IR). apply pos_half. apply leEq_wdl with ([1][-] (Half:IR)). 2: unfold Half in |- *; rational. apply shift_minus_leEq; apply shift_leEq_plus'. astepl (Exp [0][-]Exp x). eapply leEq_transitive. apply leEq_AbsIR. simpl in |- *; apply H2. split; apply less_leEq. astepr ( [--]ZeroR); apply inv_resp_less; apply pos_one. apply pos_one. split; apply less_leEq. apply leEq_less_trans with ( [--] (Min d [1])). apply inv_resp_leEq; apply Min_leEq_rht. auto. apply less_leEq_trans with (Min d [1]). auto. apply Min_leEq_rht. astepl (AbsIR [--]x). eapply leEq_wdl. 2: apply AbsIR_inv. simpl in |- *; unfold ABSIR in |- *; apply less_leEq; apply Max_less. apply less_leEq_trans with (Min d [1]); auto; apply Min_leEq_lft. apply less_leEq_trans with ( [--][--] (Min d [1])). apply inv_resp_less; auto. astepl (Min d [1]); apply Min_leEq_lft. clear H4 H3 H2 H1 d H0. apply mult_cancel_less with (Exp [--]x). apply Exp_pos'. astepl ( [--]ZeroR); apply inv_resp_less; auto. astepl ZeroR; astepr OneR; apply pos_one. apply included_imp_Continuous with realline; [ apply Continuous_Exp | repeat split ]. apply leEq_transitive with ZeroR; [ astepr ( [--]ZeroR) | apply less_leEq; apply pos_one ]. apply inv_resp_leEq; apply less_leEq; apply pos_one. Qed.
imports: CoRN.transc.TaylorSeries