proposition: Lemma Taylor_Rem_char : forall n H x Hx Hx' Hx'', F x Hx[-]FSum0 (S n) Taylor_Series x Hx' [=] Taylor_Rem J pJ F a x Ha Hx'' n H.
proof: Proof. intros; unfold Taylor_Rem in |- *; repeat apply cg_minus_wd. algebra. simpl in |- *. apply bin_op_wd_unfolded. 2: apply mult_wdl. apply eq_symmetric_unfolded. cut (ext_fun_seq' (fun (i : nat) (l : i < n) => [-C-] (N_Deriv _ _ _ _ (le_imp_Diffble_n _ _ _ _ (proj1 (Nat.lt_succ_r _ _) (Nat.lt_lt_succ_r _ _ l)) _ H) a Ha[/] _[//]nring_fac_ap_zero _ i) {*} (FId{-} [-C-]a) {^}i)). intro H0. apply eq_transitive_unfolded with (Sumx (fun (i : nat) (Hi : i < n) => Part ( [-C-] (N_Deriv _ _ _ _ (le_imp_Diffble_n _ _ _ _ (proj1 (Nat.lt_succ_r _ _) (Nat.lt_lt_succ_r _ _ Hi)) _ H) a Ha[/] _[//]nring_fac_ap_zero _ i) {*} (FId{-} [-C-]a) {^}i) x (FSumx_pred _ _ H0 _ (ProjIR1 (TaylorB _ _ _ a x Ha _ H)) i Hi))). exact (FSumx_char _ _ _ _ H0). apply Sumx_Sum0. intros; simpl in |- *. apply mult_wdl; apply div_wd. 2: algebra. apply Feq_imp_eq with J; auto. apply Derivative_n_unique with pJ i F; auto. apply N_Deriv_lemma. red in |- *; do 3 intro. rewrite H0; intros; simpl in |- *; auto. apply div_wd. 2: algebra. apply Feq_imp_eq with J; auto. apply Derivative_n_unique with pJ n F; auto. Deriv. Qed.
imports: CoRN.transc.PowerSeries CoRN.ftc.Taylor