proposition: Theorem Cor_Taylor_Lagrange (x0 x : R) : Cab x0 -> Cab x -> exists c, D 0 x - Tsum n x0 x = Tcoeff (S n) c * (x - x0)^(S n) /\ (x0 <> x -> x0 < c < x \/ x < c < x0).
proof: Proof. intros Hx0 Hx. apply Taylor_Lagrange. - intros k x1 Hk Hab; apply derivable_pt_lim_Dp; trivial. now split; case Hab; left. - intros k x1 Hk Hab. apply derivable_continuous_pt. unfold derivable_pt, derivable_pt_abs. exists (D (S k) x1). now apply derivable_pt_lim_Dp. - exact Hx0. - exact Hx. Qed.
imports: Coq(Reals Psatz) Coquelicot(Coquelicot) Stdlib