proposition: Lemma Taylor_lemma4 : forall n Hf Hab Ha', g n Hf Hab a Ha' [=] [0].
proof: Proof. unfold g in |- *; clear g; intros. cut (Dom ( [-C-] (F b Hb) {-}Taylor_seq'_aux n Hf{-} [-C-] (Taylor_rem n Hf)) a). intro H. apply eq_transitive_unfolded with (Part _ _ H). Opaque Taylor_seq'_aux Taylor_rem. simpl in |- *; rational. Transparent Taylor_rem. unfold Taylor_rem in |- *. apply eq_transitive_unfolded with (Part _ _ (TL_lemma_b n Hf) [-]Part _ _ (TL_lemma_a' n Hf)). Opaque Taylor_seq'. simpl in |- *; rational. Transparent Taylor_seq' Taylor_seq'_aux. unfold Taylor_seq', Taylor_seq'_aux in |- *. cut (Dom (FSum 0 n (FSumx_to_FSum _ (funct_i n Hf))) b). intro H0. cut (Dom (FSum 0 n (FSumx_to_FSum _ (funct_i' n Hf))) a). intro H1. apply eq_transitive_unfolded with (Part _ _ H0[-]Part _ _ H1). apply eq_symmetric_unfolded; apply cg_minus_wd; apply FSum_FSumx_to_FSum. apply Taylor_lemma2. apply Taylor_lemma2'. apply Taylor_lemma3. apply Taylor_lemma3'. eapply eq_transitive_unfolded. simpl in |- *. apply eq_symmetric_unfolded; apply Sum_minus_Sum. apply Sum_zero. auto with arith. intros. cut (forall Hb' Ha', FSumx_to_FSum (S n) (funct_i n Hf) i b Hb'[-] FSumx_to_FSum (S n) (funct_i' n Hf) i a Ha' [=] [0]); auto. unfold FSumx_to_FSum in |- *. elim le_lt_dec; intro; simpl in |- *. algebra. intros. set (w := fi n Hf i b0 (Build_subcsetoid_crr _ _ _ TL_compact_a) [*] ([1][/] _[//]nring_fac_ap_zero IR i) [*] (b[+][--]a) [^]i) in *. astepr (w[-]w); unfold w in |- *; simpl in |- *. repeat first [ apply cg_minus_wd | simple apply mult_wd ]; try apply csf_wd_unfolded; algebra. rational. simpl in |- *; algebra. simpl in |- *; intro i. Opaque funct_i'. unfold FSumx_to_FSum in |- *. elim le_lt_dec; intro; simpl in |- *. auto. apply TL_a_i'. Opaque funct_i. simpl in |- *; intro i. unfold FSumx_to_FSum in |- *. elim le_lt_dec; intro; simpl in |- *. auto. apply TL_b_i. split; split; split. apply FSumx_pred'. red in |- *; intros. inversion_clear X. inversion_clear X0. simpl in X. split; split; auto. simpl in |- *; apply compact_wd with x; auto. intros; apply TL_a_i'. apply TL_a_i'. Qed.
imports: CoRN.ftc.Rolle Coq(Lia)