proposition: Theorem Taylor : forall e, [0] [<] e -> forall Hb', {c : IR | Compact (Min_leEq_Max a b) c | forall Hc, AbsIR (F b Hb'[-]Part _ _ Taylor_aux[-]deriv_Sn c Hc[*] (b[-]a)) [<=] e}.
proof: Proof. intros e H Hb'. cut (Diffble_n (S n) I pI F). intro Hf. cut (Diffble_n n I pI F). intro Hf'. elim (Taylor' I pI F _ _ Ha Hb n Hf Hf' e H); intros c Hc' Hc. exists c. auto. intros. cut (Dom (N_Deriv _ _ _ _ Hf{*} [-C-] ([1][/] _[//]nring_fac_ap_zero IR n) {*} ( [-C-]b{-}FId) {^}n) c). intro H0. eapply leEq_wdl. apply (Hc H0). apply AbsIR_wd; simpl in |- *; repeat simple apply cg_minus_wd. 2: repeat simple apply mult_wdl. unfold Taylor_Rem in |- *; simpl in |- *. apply cg_minus_wd. algebra. apply bin_op_wd_unfolded. apply Feq_imp_eq with (Compact (Min_leEq_Max a b)). apply FSumx_wd'. unfold funct_i in |- *; intros; simpl in |- *. apply Feq_mult. FEQ. simpl in |- *. apply div_wd. apply Feq_imp_eq with I. apply Derivative_n_unique with pI i F. apply N_Deriv_lemma. apply derF. auto. algebra. apply Feq_reflexive; repeat split. apply compact_Min_rht. apply mult_wdl. apply div_wd. 2: algebra. apply Feq_imp_eq with I. apply Derivative_n_unique with pI n F. apply N_Deriv_lemma. apply derF. auto. apply Feq_imp_eq with I. apply Derivative_n_unique with pI (S n) F. apply N_Deriv_lemma. assumption. cut (included (Compact (Min_leEq_Max a b)) I); Included. repeat split. Transparent N_Deriv. simpl in |- *. cut (included (Compact (Min_leEq_Max a b)) I); Included. apply Derivative_n_imp_Diffble_n with (f n (Nat.lt_succ_diag_r n)). apply derF. apply Derivative_n_imp_Diffble_n with F'. assumption. Qed.
imports: CoRN.ftc.TaylorLemma