proposition: Lemma Taylor_majoration_lemma : forall (n : nat) (e : IR), [0] [<] e -> e[*] (nring n[/] _[//]H1 n) [<=] e.
proof: Proof. intro; case n. intros; simpl in |- *; rstepl ZeroR; apply less_leEq; auto. clear n; intro; induction n as [| n Hrecn]. intros; simpl in |- *. eapply leEq_wdl. apply less_leEq; apply pos_div_two'; auto. rational. intros e H0. eapply leEq_transitive. 2: apply Hrecn; auto. apply mult_resp_leEq_lft. 2: apply less_leEq; auto. apply shift_div_leEq. repeat apply mult_resp_pos; try apply nexp_resp_pos; apply pos_two. rstepr (nring (S n) [*]Two[^]S (S n) [/] _[//]H1 (S n)). apply shift_leEq_div. apply nexp_resp_pos; apply pos_two. Transparent nexp_op. set (p := S n) in *. cut (p = S n); [ intro | auto ]. clear H0; clearbody p. simpl in |- *; fold (Two:IR) in |- *. rstepl (nring (R:=IR) p[*]nexp _ p Two[+]nring 1[*]nexp _ p Two). rstepr (nring (R:=IR) p[*]nexp _ p Two[+]nring p[*]nexp _ p Two). apply plus_resp_leEq_lft. apply mult_resp_leEq_rht. apply nring_leEq; rewrite H2; auto with arith. astepr ((Two:IR) [^]p); apply nexp_resp_nonneg. apply less_leEq; apply pos_two. Qed.
imports: CoRN.transc.PowerSeries CoRN.ftc.Taylor