proposition: Lemma Taylor_Series_conv_lemma2 : forall x y Hxy (e : IR) (He : [0] [<] e), {N : nat | forall n : nat, N <= n -> forall z : IR, compact x y Hxy z -> forall Hz, AbsIR (Taylor_Series _ _ _ a Ha _ derF n z Hz) [<=] (e[/] _[//]H1 n)}.
proof: Proof. intros. elim Taylor_Series_conv_lemma1 with (t := a) (Hxy := Hxy) (e := e); auto. intros N HN; exists (S N). intros n H0 z H2 Hz. assert (n = S (pred n)). symmetry; apply Nat.lt_succ_pred with N; auto with arith. set (p := pred n) in *. assert (N <= p). unfold p in |- *; apply le_S_n; rewrite Nat.lt_succ_pred with N n; auto with arith. clearbody p; rewrite H3. assert (H5 : forall c d : IR, Dom (c{**} ((FId{-} [-C-]d) {^}p{*} (FId{-} [-C-]a))) z). repeat split. assert (H6 : Compact (Min_leEq_Max' x y a) a). split; [ apply Min_leEq_rht | apply rht_leEq_Max ]. eapply leEq_wdl. apply (HN p H4 a z H2 H6 Ha (H5 (Part _ _ (Derivative_n_imp_inc' _ _ _ _ _ (derF (S p)) a Ha) [/] _[//] nring_fac_ap_zero _ (S p)) a)). apply AbsIR_wd; algebra. Qed.
imports: CoRN.transc.PowerSeries CoRN.ftc.Taylor