proposition: Lemma Taylor_lemma2 : forall n Hf, ext_fun_seq (funct_i n Hf).
proof: Proof. red in |- *; intros n Hf i j H H0 H' x y H1 Hx Hy. simpl in |- *. apply mult_wd. apply div_wd. 2: rewrite H; algebra. generalize H' Hx Hy; clear Hy Hx H'. rewrite <- H; intros. cut (forall Ha1 Ha2, PartInt (fi n Hf i H0) a Ha1 [=] PartInt (fi n Hf i H') a Ha2); intros. simpl in H2. apply H2. apply Feq_imp_eq with (Compact Hab). unfold Hab in |- *; apply Derivative_I_n_unique with i F; apply Taylor_lemma1. apply TL_compact_a. rewrite H. astepl ((x[+][--]a) [^]j); Step_final ((y[+][--]a) [^]j). Qed.
imports: CoRN.ftc.Rolle Coq(Lia)