proposition: Lemma Taylor_lemma3' : forall n Hf, ext_fun_seq' (funct_i' n Hf).
proof: Proof. intros n Hf i j H H0 H' x y H1 H2. elim H2; intros. simpl in a0, b0. clear b0; inversion_clear a0 as (X,X0). inversion_clear X; repeat split. astepr x; auto. astepl x; auto. Qed.
imports: CoRN.ftc.Rolle Coq(Lia)