proposition: Lemma Taylor_lemma3 : 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 mult_wd. 2: rewrite H; algebra. generalize H' Hx Hy; clear Hy Hx H'. rewrite <- H; intros. cut (forall Hx' Hy', PartInt (fi n Hf i H0) x Hx' [=] PartInt (fi n Hf i H') y Hy'); intros. simpl in H2. apply H2. cut (Dom (PartInt (fi n Hf i H')) x); [ intro H2 | apply dom_wd with y; algebra ]. apply eq_transitive_unfolded with (Part _ _ H2). apply Feq_imp_eq with (Compact Hab). unfold Hab in |- *; apply Derivative_I_n_unique with i F; apply Taylor_lemma1. simpl in Hx. elim Hx; intros. inversion_clear a0; auto. algebra. rewrite H. astepl ((b[+][--]x) [^]j); Step_final ((b[+][--]y) [^]j). Qed.
imports: CoRN.ftc.Rolle Coq(Lia)