by (rule_tac x = "(f h - (\<Sum>m=0..<n. (j m / real (fact m)) * h^m)) *

 by (rule exI[where x = "(f h - (\<Sum>m=0..<n. (j m / real (fact m)) * h^m)) *

                  real(fact n) / (h^n)"

                  real(fact n) / (h^n)"]) simp

        in exI, simp)

   and INIT : "n = Suc k"

     and INIT : "n = Suc k"

   and DIFG_DEF: "difg = (\<lambda>m t. diff m t - ((\<Sum>p = 0..<n - m. diff (m + p) 0 / real (fact p) * t ^ p) + 

   defines "difg \<equiv> (\<lambda>m t. diff m t - ((\<Sum>p = 0..<n - m. diff (m + p) 0 / real (fact p) * t ^ p) +

   B * (t ^ (n - m) / real (fact (n - m)))))"

     B * (t ^ (n - m) / real (fact (n - m)))))" (is "difg \<equiv> (\<lambda>m t. diff m t - ?difg m t)")

 proof (rule allI)+

 proof (rule allI impI)+

   fix m

   fix m t assume INIT2: "m < n & 0 \<le> t & t \<le> h"

   fix t

   have "DERIV (difg m) t :> diff (Suc m) t -

   show "m < n \<and> 0 \<le> t \<and> t \<le> h \<longrightarrow> DERIV (difg m) t :> difg (Suc m) t"

     ((\<Sum>x = 0..<n - m. real x * t ^ (x - Suc 0) * diff (m + x) 0 / real (fact x)) +

   proof

      real (n - m) * t ^ (n - Suc m) * B / real (fact (n - m)))" unfolding difg_def

     assume INIT2: "m < n & 0 \<le> t & t \<le> h"

     by (auto intro!: DERIV_intros DERIV[rule_format, OF INIT2])

     hence INTERV: "0 \<le> t & t \<le> h" ..

     from INIT2 and INIT have mtok: "m < Suc k" by arith

     have "DERIV (\<lambda>t. diff m t -

     ((\<Sum>p = 0..<Suc k - m. diff (m + p) 0 / real (fact p) * t ^ p) +

     B * (t ^ (Suc k - m) / real (fact (Suc k - m)))))

     t :> diff (Suc m) t -

     ((\<Sum>p = 0..<Suc k - Suc m. diff (Suc m + p) 0 / real (fact p) * t ^ p) +

     B * (t ^ (Suc k - Suc m) / real (fact (Suc k - Suc m))))"

     proof -

       from DERIV and INIT2 have "DERIV (diff m) t :> diff (Suc m) t" by simp

       have " DERIV (\<lambda>x. (\<Sum>p = 0..<Suc k - m. diff (m + p) 0 / real (fact p) * x ^ p) +

   from INIT2 have intvl: "{..<n - m} = insert 0 (Suc ` {..<n - Suc m})" and "0 < n - m"

 	B * (x ^ (Suc k - m) / real (fact (Suc k - m))))

     unfolding atLeast0LessThan[symmetric] by auto

 	t :> (\<Sum>p = 0..<Suc k - Suc m. diff (Suc m + p) 0 / real (fact p) * t ^ p) +

   have "(\<Sum>x = 0..<n - m. real x * t ^ (x - Suc 0) * diff (m + x) 0 / real (fact x)) =

 	B * (t ^ (Suc k - Suc m) / real (fact (Suc k - Suc m)))"

       (\<Sum>x = 0..<n - Suc m. real (Suc x) * t ^ x * diff (Suc m + x) 0 / real (fact (Suc x)))"

       proof -

     unfolding intvl atLeast0LessThan by (subst setsum.insert) (auto simp: setsum.reindex)

 	have "DERIV (\<lambda>x. \<Sum>p = 0..<Suc k - m. diff (m + p) 0 / real (fact p) * x ^ p) t

   moreover

 	  :> (\<Sum>p = 0..<Suc k - Suc m. diff (Suc m + p) 0 / real (fact p) * t ^ p)"

   have fact_neq_0: "\<And>x::nat. real (fact x) + real x * real (fact x) \<noteq> 0"

 	proof -

     by (metis fact_gt_zero_nat not_add_less1 real_of_nat_add real_of_nat_mult real_of_nat_zero_iff)

 	  have "\<exists> d. k = m + d"

   have "\<And>x. real (Suc x) * t ^ x * diff (Suc m + x) 0 / real (fact (Suc x)) =

 	  proof -

       diff (Suc m + x) 0 * t^x / real (fact x)"

 	    from INIT2 have "m < n" ..

     by (auto simp: field_simps real_of_nat_Suc fact_neq_0 intro!: nonzero_divide_eq_eq[THEN iffD2])

 	    hence "\<exists> d. n = m + d + Suc 0" by arith

   moreover

 	    with INIT show ?thesis by (simp del: setsum_op_ivl_Suc)

   have "real (n - m) * t ^ (n - Suc m) * B / real (fact (n - m)) =

 	  qed

       B * (t ^ (n - Suc m) / real (fact (n - Suc m)))"

 	  from this obtain d where kmd: "k = m + d" ..

     using `0 < n - m` by (simp add: fact_reduce_nat)

 	  have "DERIV (\<lambda>x. (\<Sum>ma = 0..<d. diff (Suc (m + ma)) 0 * x ^ Suc ma / real (fact (Suc ma))) +

   ultimately show "DERIV (difg m) t :> difg (Suc m) t"

             diff m 0)

     unfolding difg_def by simp

 	    t :> (\<Sum>p = 0..<d. diff (Suc (m + p)) 0 * t ^ p / real (fact p))"

 qed

 	  proof - 

 	    have "DERIV (\<lambda>x. (\<Sum>ma = 0..<d. diff (Suc (m + ma)) 0 * x ^ Suc ma / real (fact (Suc ma))) + diff m 0) t :>  (\<Sum>r = 0..<d. diff (Suc (m + r)) 0 * t ^ r / real (fact r)) + 0"

 	    proof -

 	      from DERIV and INTERV have "DERIV (\<lambda>x. (\<Sum>ma = 0..<d. diff (Suc (m + ma)) 0 * x ^ Suc ma / real (fact (Suc ma)))) t :>  (\<Sum>r = 0..<d. diff (Suc (m + r)) 0 * t ^ r / real (fact r))"

 	      proof -

 		have "\<forall>r. 0 \<le> r \<and> r < 0 + d \<longrightarrow>

 		  DERIV (\<lambda>x. diff (Suc (m + r)) 0 * x ^ Suc r / real (fact (Suc r))) t

 		  :> diff (Suc (m + r)) 0 * t ^ r / real (fact r)"

 		proof (rule allI)

 		  fix r

 		  show " 0 \<le> r \<and> r < 0 + d \<longrightarrow>

 		    DERIV (\<lambda>x. diff (Suc (m + r)) 0 * x ^ Suc r / real (fact (Suc r))) t

 		    :> diff (Suc (m + r)) 0 * t ^ r / real (fact r)"

 		  proof 

 		    assume "0 \<le> r & r < 0 + d"

 		    have "DERIV (\<lambda>x. diff (Suc (m + r)) 0 *

                       (x ^ Suc r * inverse (real (fact (Suc r)))))

 		      t :> diff (Suc (m + r)) 0 * (t ^ r * inverse (real (fact r)))"

 		    proof -

                       have "(1 + real r) * real (fact r) \<noteq> 0" by auto

 		      from this have "real (fact r) + real r * real (fact r) \<noteq> 0"

                         by (metis add_nonneg_eq_0_iff mult_nonneg_nonneg real_of_nat_fact_not_zero real_of_nat_ge_zero)

                       from this have "DERIV (\<lambda>x. x ^ Suc r * inverse (real (fact (Suc r)))) t :> real (Suc r) * t ^ (Suc r - Suc 0) * inverse (real (fact (Suc r))) +

 			0 * t ^ Suc r"

                         apply - by ( rule DERIV_intros | rule refl)+ auto

 		      moreover

 		      have "real (Suc r) * t ^ (Suc r - Suc 0) * inverse (real (fact (Suc r))) +

 			0 * t ^ Suc r =

 			t ^ r * inverse (real (fact r))"

 		      proof -

 			have " real (Suc r) * t ^ (Suc r - Suc 0) *

 			  inverse (real (Suc r) * real (fact r)) +

 			  0 * t ^ Suc r =

 			  t ^ r * inverse (real (fact r))" by (simp add: mult_ac)

 			hence "real (Suc r) * t ^ (Suc r - Suc 0) * inverse (real (Suc r * fact r)) +

 			  0 * t ^ Suc r =

 			  t ^ r * inverse (real (fact r))" by (subst real_of_nat_mult)

 			thus ?thesis by (subst fact_Suc)

 		      qed

 		      ultimately have " DERIV (\<lambda>x. x ^ Suc r * inverse (real (fact (Suc r)))) t

 			:> t ^ r * inverse (real (fact r))" by (rule lemma_DERIV_subst)

 		      thus ?thesis by (rule DERIV_cmult)

 		    qed

 		    thus "DERIV (\<lambda>x. diff (Suc (m + r)) 0 * x ^ Suc r /

                       real (fact (Suc r)))

 		      t :> diff (Suc (m + r)) 0 * t ^ r / real (fact r)" by (simp (no_asm) add: divide_inverse mult_assoc del: fact_Suc power_Suc)

 		  qed

 		qed

 		thus ?thesis by (rule DERIV_sumr)

 	      qed

 	      moreover

 	      from DERIV_const have "DERIV (\<lambda>x. diff m 0) t :> 0" .

 	      ultimately show ?thesis by (rule DERIV_add)

 	    qed

 	    moreover

 	    have " (\<Sum>r = 0..<d. diff (Suc (m + r)) 0 * t ^ r / real (fact r)) + 0 =  (\<Sum>p = 0..<d. diff (Suc (m + p)) 0 * t ^ p / real (fact p))"  by simp

 	    ultimately show ?thesis by (rule lemma_DERIV_subst)

 	  qed

 	  with kmd and sumr_offset4 [of 1] show ?thesis by (simp del: setsum_op_ivl_Suc fact_Suc power_Suc)

 	qed

 	moreover

 	have " DERIV (\<lambda>x. B * (x ^ (Suc k - m) / real (fact (Suc k - m)))) t

 	  :> B * (t ^ (Suc k - Suc m) / real (fact (Suc k - Suc m)))"

 	proof -

 	  have " DERIV (\<lambda>x. x ^ (Suc k - m) / real (fact (Suc k - m))) t

 	    :> t ^ (Suc k - Suc m) / real (fact (Suc k - Suc m))"

 	  proof -

 	    have "DERIV (\<lambda>x. x ^ (Suc k - m)) t :> real (Suc k - m) * t ^ (Suc k - m - Suc 0)" by (rule DERIV_pow)

 	    moreover

 	    have "DERIV (\<lambda>x. real (fact (Suc k - m))) t :> 0" by (rule DERIV_const)

 	    moreover

 	    have "(\<lambda>x. real (fact (Suc k - m))) t \<noteq> 0" by simp

 	    ultimately have " DERIV (\<lambda>y. y ^ (Suc k - m) / real (fact (Suc k - m))) t

 	      :>  ( real (Suc k - m) * t ^ (Suc k - m - Suc 0) * real (fact (Suc k - m)) + - (0 * t ^ (Suc k - m))) /

 	      real (fact (Suc k - m)) ^ Suc (Suc 0)"

               apply -

               apply (rule DERIV_cong) by (rule DERIV_intros | rule refl)+ auto

 	    moreover

 	    from mtok and INIT have "( real (Suc k - m) * t ^ (Suc k - m - Suc 0) * real (fact (Suc k - m)) + - (0 * t ^ (Suc k - m))) /

 	      real (fact (Suc k - m)) ^ Suc (Suc 0) =  t ^ (Suc k - Suc m) / real (fact (Suc k - Suc m))" by (simp add: fact_diff_Suc)

 	    ultimately show ?thesis by (rule lemma_DERIV_subst)

 	  qed

 	  moreover

 	  thus ?thesis by (rule DERIV_cmult)

 	qed

 	ultimately show ?thesis by (rule DERIV_add)

       qed

       ultimately show ?thesis by (rule DERIV_diff) 

     qed

     from INIT and this and DIFG_DEF show "DERIV (difg m) t :> difg (Suc m) t" by clarify

   qed

 qed

               (diff n t / real (fact n)) * h ^ n"  

               (diff n t / real (fact n)) * h ^ n"

     by (cases n, simp add: n)

     by (cases n) (simp add: n)

   obtain g where g_def: "g = (%t. f t -

   def g \<equiv> "(\<lambda>t. f t -

     (setsum (%m. (diff m 0 / real(fact m)) * t^m) {0..<n}

     (setsum (\<lambda>m. (diff m 0 / real(fact m)) * t^m) {0..<n}

       + (B * (t^n / real(fact n)))))" by blast

       + (B * (t^n / real(fact n)))))"

   obtain difg where difg_def: "difg = (%m t. diff m t -

   def difg \<equiv> "(%m t. diff m t -

       + (B * ((t ^ (n - m)) / real (fact (n - m))))))" by blast

       + (B * ((t ^ (n - m)) / real (fact (n - m))))))"

     using diff_Suc m difg_def by (rule Maclaurin_lemma2)

     using diff_Suc m unfolding difg_def by (rule Maclaurin_lemma2)

   case 0

     case 0

   case (Suc m')

     case (Suc m')

   case Suc 

   case Suc

     (\<Sum>m = 0..<n. diff m 0 / real (fact m) * h ^ m) + diff n t / real (fact n) * h ^ n" 

     (\<Sum>m = 0..<n. diff m 0 / real (fact m) * h ^ m) + diff n t / real (fact n) * h ^ n"

   assumes INTERV : "h < 0" and

   assumes "h < 0" "0 < n" "diff 0 = f"

   INIT : "0 < n" "diff 0 = f" and

   and DERIV: "\<forall>m t. m < n & h \<le> t & t \<le> 0 --> DERIV (diff m) t :> diff (Suc m) t"

              ABL : "\<forall>m t. m < n & h \<le> t & t \<le> 0 --> DERIV (diff m) t :> diff (Suc m) t"

   from INTERV have "0 < -h" by simp

   txt "Transform @{text ABL'} into @{text DERIV_intros} format."

   moreover

   note DERIV' = DERIV_chain'[OF _ DERIV[rule_format], THEN DERIV_cong]

   from INIT have "0 < n" by simp

   from assms

   moreover

   have "\<exists>t>0. t < - h \<and>

   from INIT have "(% x. ( - 1) ^ 0 * diff 0 (- x)) = (% x. f (- x))" by simp

   moreover

   have "\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> - h \<longrightarrow>

     DERIV (\<lambda>x. (- 1) ^ m * diff m (- x)) t :> (- 1) ^ Suc m * diff (Suc m) (- t)"

   proof (rule allI impI)+

     fix m t

     assume tINTERV:" m < n \<and> 0 \<le> t \<and> t \<le> - h"

     with ABL show "DERIV (\<lambda>x. (- 1) ^ m * diff m (- x)) t :> (- 1) ^ Suc m * diff (Suc m) (- t)"

     proof -

       from ABL and tINTERV have "DERIV (\<lambda>x. diff m (- x)) t :> - diff (Suc m) (- t)" (is ?tABL)

       proof -

 	from ABL and tINTERV have "DERIV (diff m) (- t) :> diff (Suc m) (- t)" by force

 	moreover

 	from DERIV_ident[of t] have "DERIV uminus t :> (- 1)" by (rule DERIV_minus) 

 	ultimately have "DERIV (\<lambda>x. diff m (- x)) t :> diff (Suc m) (- t) * - 1" by (rule DERIV_chain2)

 	thus ?thesis by simp

       qed

       thus ?thesis

       proof -

 	assume ?tABL hence "DERIV (\<lambda>x. -1 ^ m * diff m (- x)) t :> -1 ^ m * - diff (Suc m) (- t)" by (rule DERIV_cmult)

 	hence "DERIV (\<lambda>x. -1 ^ m * diff m (- x)) t :> - (-1 ^ m * diff (Suc m) (- t))" by (subst minus_mult_right)

 	thus ?thesis by simp 

       qed

     qed

   qed

   ultimately have t_exists: "\<exists>t>0. t < - h \<and>

     (- 1) ^ n * diff n (- t) / real (fact n) * (- h) ^ n" (is "\<exists> t. ?P t") by (rule Maclaurin)

     (- 1) ^ n * diff n (- t) / real (fact n) * (- h) ^ n"

   from this obtain t where t_def: "?P t" ..

     by (intro Maclaurin) (auto intro!: DERIV_intros DERIV')

   then guess t ..

 by (induct "n", auto)

 by (induct "n") auto

    assumes INIT : "diff 0 = f"

    assumes "diff 0 = f"

               diff n t / real (fact n) * x ^ n"

      diff n t / real (fact n) * x ^ n" (is "\<exists>t. _ \<and> f x = ?f x t")

 proof (cases "n = 0")

 proof cases

   case True from INIT True show ?thesis by force

   assume "n = 0" with `diff 0 = f` show ?thesis by force

   case False

   assume "n \<noteq> 0"

   from this have n_not_zero:"n \<noteq> 0" .

   show ?thesis

   from False INIT DERIV show ?thesis

   proof (cases rule: linorder_cases)

   proof (cases "x = 0")

     assume "x = 0" with `n \<noteq> 0` `diff 0 = f` DERIV

     case True show ?thesis

     have "\<bar>0\<bar> \<le> \<bar>x\<bar> \<and> f x = ?f x 0" by (force simp add: Maclaurin_bi_le_lemma)

     proof -

     thus ?thesis ..

       from n_not_zero True INIT DERIV have "\<bar>0\<bar> \<le> \<bar>x\<bar> \<and>

 	f x = (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n 0 / real (fact n) * x ^ n" by(force simp add: Maclaurin_bi_le_lemma) 

       thus ?thesis ..

     qed

     case False 

     assume "x < 0"

     note linorder_less_linear [of "x" "0"] 

     with `n \<noteq> 0` DERIV

     thus ?thesis

     have "\<exists>t>x. t < 0 \<and> diff 0 x = ?f x t" by (intro Maclaurin_minus) auto

     proof (elim disjE)

     then guess t ..

       assume "x = 0" with False show ?thesis ..

     with `x < 0` `diff 0 = f` have "\<bar>t\<bar> \<le> \<bar>x\<bar> \<and> f x = ?f x t" by simp

       next

     thus ?thesis ..

       assume x_less_zero: "x < 0" moreover

   next

       from n_not_zero have "0 < n" by simp moreover

     assume "x > 0"

       have "diff 0 = diff 0" by simp moreover

     with `n \<noteq> 0` `diff 0 = f` DERIV

       have "\<forall>m t. m < n \<and> x \<le> t \<and> t \<le> 0 \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"

     have "\<exists>t>0. t < x \<and> diff 0 x = ?f x t" by (intro Maclaurin) auto

       proof (rule allI, rule allI, rule impI)

     then guess t ..

 	fix m t

     with `x > 0` `diff 0 = f` have "\<bar>t\<bar> \<le> \<bar>x\<bar> \<and> f x = ?f x t" by simp

 	assume "m < n & x \<le> t & t \<le> 0"

     thus ?thesis ..

 	with DERIV show " DERIV (diff m) t :> diff (Suc m) t" by (fastsimp simp add: abs_if)

       qed

       ultimately have t_exists:"\<exists>t>x. t < 0 \<and>

         diff 0 x =

         (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n t / real (fact n) * x ^ n" (is "\<exists> t. ?P t") by (rule Maclaurin_minus)

       from this obtain t where t_def: "?P t" ..

       from t_def x_less_zero INIT  have "\<bar>t\<bar> \<le> \<bar>x\<bar> \<and>

 	f x = (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n t / real (fact n) * x ^ n"

 	by (simp add: abs_if order_less_le)

       thus ?thesis by (rule exI)

     next

     assume x_greater_zero: "x > 0" moreover

     from n_not_zero have "0 < n" by simp moreover

     have "diff 0 = diff 0" by simp moreover

     have "\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> x \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"

       proof (rule allI, rule allI, rule impI)

 	fix m t

 	assume "m < n & 0 \<le> t & t \<le> x"

 	with DERIV show " DERIV (diff m) t :> diff (Suc m) t" by fastsimp

       qed

       ultimately have t_exists:"\<exists>t>0. t < x \<and>

         diff 0 x =

         (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n t / real (fact n) * x ^ n" (is "\<exists> t. ?P t") by (rule Maclaurin)

       from this obtain t where t_def: "?P t" ..

       from t_def x_greater_zero INIT  have "\<bar>t\<bar> \<le> \<bar>x\<bar> \<and>

 	f x = (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n t / real (fact n) * x ^ n"

 	by fastsimp

       thus ?thesis ..

     qed

   shows "\<exists>t. 0 < abs t & abs t < abs x &

   shows "\<exists>t. 0 < abs t & abs t < abs x & f x =

                f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +

     (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +

                      (diff n t / real (fact n)) * x ^ n" 

                 (diff n t / real (fact n)) * x ^ n" (is "\<exists>t. _ \<and> _ \<and> f x = ?f x t")

 proof -

 proof (cases rule: linorder_cases)

   have "(x = 0) \<Longrightarrow> ?thesis"

   assume "x = 0" with INIT3 show "?thesis"..

   proof -

 next

     assume "x = 0"

   assume "x < 0"

     with INIT3 show "(x = 0) \<Longrightarrow> ?thesis"..

   with assms have "\<exists>t>x. t < 0 \<and> f x = ?f x t" by (intro Maclaurin_minus) auto

   qed

   then guess t ..

   moreover have "(x < 0) \<Longrightarrow> ?thesis"

   with `x < 0` have "0 < \<bar>t\<bar> \<and> \<bar>t\<bar> < \<bar>x\<bar> \<and> f x = ?f x t" by simp

   proof -

   thus ?thesis ..

     assume x_less_zero: "x < 0"

 next

     from DERIV have "\<forall>m t. m < n \<and> x \<le> t \<and> t \<le> 0 \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t" by simp 

   assume "x > 0"

     with x_less_zero INIT2 INIT1 have "\<exists>t>x. t < 0 \<and> f x = (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n t / real (fact n) * x ^ n" (is "\<exists> t. ?P t") by (rule Maclaurin_minus)

   with assms have "\<exists>t>0. t < x \<and> f x = ?f x t " by (intro Maclaurin) auto

     from this obtain t where "?P t" ..

   then guess t ..

     with x_less_zero have "0 < \<bar>t\<bar> \<and>

   with `x > 0` have "0 < \<bar>t\<bar> \<and> \<bar>t\<bar> < \<bar>x\<bar> \<and> f x = ?f x t" by simp

       \<bar>t\<bar> < \<bar>x\<bar> \<and>

   thus ?thesis ..

       f x = (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n t / real (fact n) * x ^ n" by simp

     thus ?thesis ..

   qed

   moreover have "(x > 0) \<Longrightarrow> ?thesis"

   proof -

     assume x_greater_zero: "x > 0"

     from DERIV have "\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> x \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t" by simp

     with x_greater_zero INIT2 INIT1 have "\<exists>t>0. t < x \<and> f x = (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n t / real (fact n) * x ^ n" (is "\<exists> t. ?P t") by (rule Maclaurin)

     from this obtain t where "?P t" ..

     with x_greater_zero have "0 < \<bar>t\<bar> \<and>

       \<bar>t\<bar> < \<bar>x\<bar> \<and>

       f x = (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n t / real (fact n) * x ^ n" by fastsimp

     thus ?thesis ..

   qed

   ultimately show ?thesis by (fastsimp) 

   shows "\<exists>t. abs t \<le> abs x &

   shows "\<exists>t. abs t \<le> abs x & f x =

               f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +

     (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +

                     (diff n t / real (fact n)) * x ^ n"

     (diff n t / real (fact n)) * x ^ n" (is "\<exists>t. _ \<and> f x = ?f x t")

 proof -

 proof cases

   note linorder_le_less_linear [of n 0]

   assume "n = 0" with INIT show ?thesis by force

   thus ?thesis

   proof

     assume "n\<le> 0" with INIT show ?thesis by force

     assume n_greater_zero: "n > 0" show ?thesis

   assume "n \<noteq> 0"

     proof (cases "x = 0")

   show ?thesis

       case True

   proof cases

       from n_greater_zero have "n \<noteq> 0" by auto

     assume "x = 0"

       from True this  have f_0:"(\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) = diff 0 0" by (rule Maclaurin_zero)

     with `n \<noteq> 0` have "(\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) = diff 0 0"

       from n_greater_zero have "n \<noteq> 0" by (rule gr_implies_not0)

       by (intro Maclaurin_zero) auto

       hence "\<exists> m. n = Suc m" by (rule not0_implies_Suc)

     with INIT `x = 0` `n \<noteq> 0` have " \<bar>0\<bar> \<le> \<bar>x\<bar> \<and> f x = ?f x 0" by force

       with f_0 True INIT have " \<bar>0\<bar> \<le> \<bar>x\<bar> \<and>

     thus ?thesis ..

        f x = (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n 0 / real (fact n) * x ^ n"

   next

 	by force

     assume "x \<noteq> 0"

       thus ?thesis ..

     with INIT `n \<noteq> 0` DERIV have "\<exists>t. 0 < \<bar>t\<bar> \<and> \<bar>t\<bar> < \<bar>x\<bar> \<and> f x = ?f x t"

     next

       by (intro Maclaurin_all_lt) auto

       case False

     then guess t ..

       from INIT n_greater_zero this DERIV have "\<exists>t. 0 < \<bar>t\<bar> \<and>

     hence "\<bar>t\<bar> \<le> \<bar>x\<bar> \<and> f x = ?f x t" by simp

 	\<bar>t\<bar> < \<bar>x\<bar> \<and> f x = (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n t / real (fact n) * x ^ n" (is "\<exists> t. ?P t") by (rule Maclaurin_all_lt)

     thus ?thesis ..

       from this obtain t where "?P t" ..

       hence "\<bar>t\<bar> \<le> \<bar>x\<bar> \<and>

        f x = (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n t / real (fact n) * x ^ n" by (simp add: order_less_le)

       thus ?thesis ..

     qed

      "sin (x + real (Suc m) * pi / 2) =  

      "sin (x + real (Suc m) * pi / 2) =

 apply (insert Maclaurin_sin_expansion2 [of x n]) 

 apply (insert Maclaurin_sin_expansion2 [of x n])

 apply (blast intro: elim:); 

 apply (blast intro: elim:)

                    simp add: est mult_nonneg_nonneg mult_ac divide_inverse

                 simp add: est mult_nonneg_nonneg mult_ac divide_inverse