proposition: Lemma Taylor_lemma10 : forall n Hf Hf' Hab (H : a [#] b), Derivative_I Hab' (g n Hf Hab) (g' n Hf Hf' Hab).
proof: Proof. unfold g, g' in |- *. intros. cut (Derivative_I Hab' (Taylor_seq'_aux n Hf) (funct_aux n Hf' n (Nat.lt_succ_diag_r n))); [ intro | apply Taylor_lemma9; assumption ]. Opaque Taylor_rem funct_aux. New_Deriv. apply Feq_reflexive; Lazy_Included. Included. apply eq_imp_Feq. Lazy_Included. Included. Lazy_Included. Included. intros; simpl in |- *; rational. Qed.
imports: CoRN.ftc.Rolle Coq(Lia)