proposition: Lemma Taylor_lemma : forall n Hf Hf', {c : IR | I c | forall Hc, AbsIR (Taylor_rem n Hf[-]deriv_Sn' n Hf' c Hc[*] (b[-]a)) [<=] e}.
proof: Proof. intros. assert (H := TLH). cut {c : IR | I c | forall Hc, AbsIR (g' n Hf Hf' H c Hc) [<=] e[*]AbsIR ([1][/] _[//]H)}; [ intro H0 | apply Taylor_lemma11; assumption ]. elim H0; intros c Hc' Hc; clear H0; exists c. auto. intro. cut (Dom (funct_aux n Hf' n (Nat.lt_succ_diag_r n)) c). intro H0. apply leEq_wdl with (AbsIR (((Taylor_rem n Hf[/] _[//]H) [-]Part _ _ H0) [*] (b[-]a))). eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply AbsIR_resp_mult. apply shift_mult_leEq with (AbsIR_resp_ap_zero _ H). apply AbsIR_pos; apply H. rstepr (e[*] ([1][/] _[//]AbsIR_resp_ap_zero _ H)). apply leEq_wdr with (e[*]AbsIR ([1][/] _[//]H)). Opaque funct_aux. cut (Dom (g' n Hf Hf' H) c). intro H1. eapply leEq_wdl. apply (Hc H1). apply AbsIR_wd; unfold g' in |- *. Opaque Taylor_rem. simpl in |- *; rational. repeat (split; auto). apply mult_wdr. apply AbsIR_recip. apply eq_symmetric_unfolded. apply eq_transitive_unfolded with (AbsIR ((Taylor_rem n Hf[/] _[//]H) [-]Part _ _ H0) [*]AbsIR (b[-]a)). eapply eq_transitive_unfolded. 2: apply AbsIR_resp_mult. apply AbsIR_wd. rstepr (Taylor_rem n Hf[-]Part _ _ H0[*] (b[-]a)). apply cg_minus_wd. algebra. apply mult_wdl. Transparent Taylor_rem funct_aux. unfold deriv_Sn', funct_aux in |- *. cut (Dom (n_deriv_I _ _ Hab' (S n) F Hf') c). intro H1. simpl in |- *; apply eq_transitive_unfolded with (n_deriv_I _ _ Hab' (S n) F Hf' c H1[*] ([1][/] _[//]nring_fac_ap_zero _ n) [*] (b[-]c) [^]n). repeat apply mult_wdl; apply pfwdef; algebra. repeat apply mult_wdl. apply eq_transitive_unfolded with (PartInt (fi (S n) Hf' (S n) (proj1 (Nat.succ_lt_mono _ _) (Nat.lt_succ_diag_r _))) c Hc'). 2: simpl in |- *; apply csf_wd_unfolded; simpl in |- *; algebra. apply Feq_imp_eq with (Compact Hab). unfold Hab in |- *; apply Derivative_I_n_unique with (S n) F. apply n_deriv_lemma. apply Taylor_lemma1. auto. apply n_deriv_inc; auto. apply eq_symmetric_unfolded; apply AbsIR_resp_mult. repeat (split; auto). Qed.
imports: CoRN.ftc.Rolle Coq(Lia)