proposition: Lemma Taylor_lemma5 : forall n Hf Hab Hb', g n Hf Hab b Hb' [=] [0].
proof: Proof. unfold g in |- *; intros. cut (Dom ( [-C-] (F b Hb) {-}Taylor_seq'_aux n Hf) b). intro H. apply eq_transitive_unfolded with (Part _ _ H). Opaque Taylor_seq'_aux. simpl in |- *; rational. Transparent Taylor_seq'_aux. unfold Taylor_seq'_aux in |- *. cut (Dom (FSum 0 n (FSumx_to_FSum _ (funct_i' n Hf))) b). intro H0. apply eq_transitive_unfolded with (F b Hb[-]Part _ _ H0). Opaque FSumx. apply eq_transitive_unfolded with (F b Hb[-]FSumx (S n) (funct_i' n Hf) b (ProjIR2 H)). simpl in |- *; rational. apply cg_minus_wd. algebra. apply eq_symmetric_unfolded; apply FSum_FSumx_to_FSum. apply Taylor_lemma3. apply Taylor_lemma3'. simpl in |- *. astepr (Part _ _ Hb[-]Part _ _ Hb); apply cg_minus_wd. algebra. eapply eq_transitive_unfolded. apply Sum_first. astepr (Part _ _ Hb[+][0]); apply bin_op_wd_unfolded. cut (forall H', FSumx_to_FSum (S n) (funct_i' n Hf) 0 b H' [=] Part _ _ Hb); auto. unfold FSumx_to_FSum in |- *. elim le_lt_dec; intro; simpl in |- *. exfalso; inversion a0. intros; simpl in |- *. rstepr (Part _ _ Hb[*][1][*][1]). apply mult_wdl. apply mult_wd. 2: rational. apply eq_symmetric_unfolded. apply eq_transitive_unfolded with (PartInt (fi n Hf 0 b0) b TL_compact_b). 2: simpl in |- *; apply csf_wd_unfolded; simpl in |- *; algebra. apply Feq_imp_eq with (Compact Hab). apply (ProjT2 (Diffble_I_n_imp_deriv_n _ _ _ _ _ (le_imp_Diffble_I _ _ _ _ _ (proj1 (Nat.lt_succ_r 0 n) b0) _ Hf))). apply TL_compact_b. apply Sum_zero. auto with arith. intros. cut (forall H', FSumx_to_FSum (S n) (funct_i' n Hf) i b H' [=] [0]); auto. unfold FSumx_to_FSum in |- *. elim le_lt_dec; intro; simpl in |- *. algebra. intro. astepr (fi n Hf i b0 (Build_subcsetoid_crr IR _ b (ProjIR1 (ProjIR1 H'))) [*] ([1][/] _[//]nring_fac_ap_zero _ i) [*][0]). apply mult_wdr. astepl ((b[-]b) [^]i). Step_final (ZeroR[^]i). intro i. Opaque funct_i'. unfold FSumx_to_FSum in |- *. elim le_lt_dec; intro; simpl in |- *. auto. apply TL_b_i'. split. simpl in |- *; auto. simpl in |- *. apply TL_lemma_b'. Qed.
imports: CoRN.ftc.Rolle Coq(Lia)