proposition: Lemma derivable_pt_lim_aux (y : R) : Oab y -> derivable_pt_lim g y (- ((D (S n) y) / (INR (fact n)) * (x - y)^n) + c * (INR (S n)) * (x - y)^n).
proof: Proof. intros Hy. unfold g. apply derivable_pt_lim_eq with ((fun y : R => (D 0 x - Tsum n y x)%R) + (fun y : R => - c *(x-y)^(S n))%R)%F. intros t; unfold plus_fct; simpl; ring. apply derivable_pt_lim_plus. - change (fun x1 : R => (D 0 x - Tsum n x1 x)%R) with ((fun x1 : R => D 0 x)%R - (fun x1 => Tsum n x1 x)%R)%F. rewrite <-Rminus_0_l. apply derivable_pt_lim_minus. now apply derivable_pt_lim_const. assert (Hdtt : forall i : nat, (i <= n)%nat -> derivable_pt_lim (fun x1 : R => Tterm i x1 x) y (/ INR (fact i) * D (S i) y * (x - y) ^ i + (Tcoeff i y) * ((INR i * (x - y) ^ pred i) * (-1)))). { intros i Hi. change (fun y : R => (Tcoeff i y * (x - y) ^ i)%R) with ((fun y : R => Tcoeff i y) * (fun y => (x - y) ^ i)%R)%F. assert (Hmul := derivable_pt_lim_mult (fun y0 : R => Tcoeff i y0) (fun y0 : R => (x - y0) ^ i) y (/ INR (fact i) * D (S i) y) ((INR i * (x - y) ^ pred i) * -(1))). simpl in Hmul. apply Hmul; clear Hmul. - unfold Rdiv. apply derivable_pt_lim_eq with (mult_real_fct (/ INR (fact i)) (D i))%R. now intros; unfold mult_real_fct; rewrite Rmult_comm. apply derivable_pt_lim_scal. now apply derivable_pt_lim_Dp. - apply derivable_pt_lim_eq with (comp (fun y => y ^ i) (fun y => x - y)). now intros y'; unfold comp. apply derivable_pt_lim_comp; [|apply derivable_pt_lim_pow]. rewrite <-Rminus_0_l. apply derivable_pt_lim_minus. now apply derivable_pt_lim_const. now apply derivable_pt_lim_id. } assert (Hs := derivable_pt_lim_sum (fun n x1 => Tterm n x1 x) y (fun i => / INR (fact i) * D (S i) y * (x - y) ^ i + D i y / INR (fact i) * (INR i * (x - y) ^ pred i * -1)) Hdtt). simpl in Hs. replace (D (S n) y / INR (fact n) * (x - y) ^ n) with (sum_f_R0 (fun i : nat => / INR (fact i) * D (S i) y * (x - y) ^ i + D i y / INR (fact i) * (INR i * (x - y) ^ pred i * -1)) n). now apply Hs. rewrite sum_eq with _ (fun i : nat => D (S i) y * / INR (fact i) * (x + - y) ^ i - D i y / INR (fact i) * INR i * (x + - y) ^ pred i) n. + elim n; [simpl; field|intros n' IHn]. simpl sum_f_R0. rewrite IHn. assert (Hinr : INR (S n') = match n' with 0%nat => 1 | S _ => INR n' + 1 end) by easy. rewrite <-Hinr. change (fact n' + n' * fact n')%nat with (fact (S n')). replace (D (S n') y / INR (fact (S n')) * INR (S n')) with (D (S n') y / INR (fact n')). change ((x + - y) * (x + - y) ^ n') with ((x + - y) ^ S n'). unfold Rdiv, Rminus; ring. replace (fact (S n')) with (fact n' * (S n'))%nat. rewrite mult_INR; unfold Rdiv; field. split; apply not_0_INR; [easy|apply fact_neq_0]. simpl; ring. + intros i Hi; unfold Rdiv, Rminus; ring. - replace (c * INR (S n) * (x - y)^n) with (- c * (INR (S n) * (x - y)^ pred (S n) * -(1))) by (simpl ; ring). apply derivable_pt_lim_scal. apply derivable_pt_lim_eq with (comp (fun y => y ^ (S n)) (fun y => x - y)). now intros y'; unfold comp. apply derivable_pt_lim_comp; [|now apply derivable_pt_lim_pow]. rewrite <-Rminus_0_l. apply derivable_pt_lim_minus. now apply derivable_pt_lim_const. now apply derivable_pt_lim_id. Qed.
imports: Coq(Reals Psatz) Coquelicot(Coquelicot) Stdlib