An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!

--- a/src/HOL/Complex.thy	Fri Feb 19 13:40:50 2016 +0100
+++ b/src/HOL/Complex.thy	Mon Feb 22 14:37:56 2016 +0000
@@ -167,10 +167,10 @@
 lemma Im_divide_numeral [simp]: "Im (z / numeral w) = Im z / numeral w"
   by (simp add: Im_divide sqr_conv_mult)
 
-lemma Re_divide_of_nat: "Re (z / of_nat n) = Re z / of_nat n"
+lemma Re_divide_of_nat [simp]: "Re (z / of_nat n) = Re z / of_nat n"
   by (cases n) (simp_all add: Re_divide divide_simps power2_eq_square del: of_nat_Suc)
 
-lemma Im_divide_of_nat: "Im (z / of_nat n) = Im z / of_nat n"
+lemma Im_divide_of_nat [simp]: "Im (z / of_nat n) = Im z / of_nat n"
   by (cases n) (simp_all add: Im_divide divide_simps power2_eq_square del: of_nat_Suc)
 
 lemma of_real_Re [simp]:
@@ -330,6 +330,12 @@
 lemma cmod_plus_Re_le_0_iff: "cmod z + Re z \<le> 0 \<longleftrightarrow> Re z = - cmod z"
   using abs_Re_le_cmod[of z] by auto
 
+lemma cmod_Re_le_iff: "Im x = Im y \<Longrightarrow> cmod x \<le> cmod y \<longleftrightarrow> abs (Re x) \<le> abs (Re y)"
+  by (metis add.commute add_le_cancel_left norm_complex_def real_sqrt_abs real_sqrt_le_iff)
+
+lemma cmod_Im_le_iff: "Re x = Re y \<Longrightarrow> cmod x \<le> cmod y \<longleftrightarrow> abs (Im x) \<le> abs (Im y)"
+  by (metis add_le_cancel_left norm_complex_def real_sqrt_abs real_sqrt_le_iff)
+
 lemma Im_eq_0: "\<bar>Re z\<bar> = cmod z \<Longrightarrow> Im z = 0"
   by (subst (asm) power_eq_iff_eq_base[symmetric, where n=2])
      (auto simp add: norm_complex_def)

--- a/src/HOL/Conditionally_Complete_Lattices.thy	Fri Feb 19 13:40:50 2016 +0100
+++ b/src/HOL/Conditionally_Complete_Lattices.thy	Mon Feb 22 14:37:56 2016 +0000
@@ -646,4 +646,44 @@
 apply (metis eq cSUP_upper)
 done 
 
+lemma cSUP_UNION:
+  fixes f :: "_ \<Rightarrow> 'b::conditionally_complete_lattice"
+  assumes ne: "A \<noteq> {}" "\<And>x. x \<in> A \<Longrightarrow> B(x) \<noteq> {}"
+      and bdd_UN: "bdd_above (\<Union>x\<in>A. f ` B x)"
+  shows "(SUP z : \<Union>x\<in>A. B x. f z) = (SUP x:A. SUP z:B x. f z)"
+proof -
+  have bdd: "\<And>x. x \<in> A \<Longrightarrow> bdd_above (f ` B x)"
+    using bdd_UN by (meson UN_upper bdd_above_mono)
+  obtain M where "\<And>x y. x \<in> A \<Longrightarrow> y \<in> B(x) \<Longrightarrow> f y \<le> M"
+    using bdd_UN by (auto simp: bdd_above_def)
+  then have bdd2: "bdd_above ((\<lambda>x. SUP z:B x. f z) ` A)"
+    unfolding bdd_above_def by (force simp: bdd cSUP_le_iff ne(2))
+  have "(SUP z:\<Union>x\<in>A. B x. f z) \<le> (SUP x:A. SUP z:B x. f z)"
+    using assms by (fastforce simp add: intro!: cSUP_least intro: cSUP_upper2 simp: bdd2 bdd)
+  moreover have "(SUP x:A. SUP z:B x. f z) \<le> (SUP z:\<Union>x\<in>A. B x. f z)"
+    using assms by (fastforce simp add: intro!: cSUP_least intro: cSUP_upper simp: image_UN bdd_UN)
+  ultimately show ?thesis
+    by (rule order_antisym)
+qed
+
+lemma cINF_UNION:
+  fixes f :: "_ \<Rightarrow> 'b::conditionally_complete_lattice"
+  assumes ne: "A \<noteq> {}" "\<And>x. x \<in> A \<Longrightarrow> B(x) \<noteq> {}"
+      and bdd_UN: "bdd_below (\<Union>x\<in>A. f ` B x)"
+  shows "(INF z : \<Union>x\<in>A. B x. f z) = (INF x:A. INF z:B x. f z)"
+proof -
+  have bdd: "\<And>x. x \<in> A \<Longrightarrow> bdd_below (f ` B x)"
+    using bdd_UN by (meson UN_upper bdd_below_mono)
+  obtain M where "\<And>x y. x \<in> A \<Longrightarrow> y \<in> B(x) \<Longrightarrow> f y \<ge> M"
+    using bdd_UN by (auto simp: bdd_below_def)
+  then have bdd2: "bdd_below ((\<lambda>x. INF z:B x. f z) ` A)"
+    unfolding bdd_below_def by (force simp: bdd le_cINF_iff ne(2))
+  have "(INF z:\<Union>x\<in>A. B x. f z) \<le> (INF x:A. INF z:B x. f z)"
+    using assms by (fastforce simp add: intro!: cINF_greatest intro: cINF_lower simp: bdd2 bdd)
+  moreover have "(INF x:A. INF z:B x. f z) \<le> (INF z:\<Union>x\<in>A. B x. f z)"
+    using assms  by (fastforce simp add: intro!: cINF_greatest intro: cINF_lower2  simp: bdd bdd_UN bdd2)
+  ultimately show ?thesis
+    by (rule order_antisym)
+qed
+
 end

--- a/src/HOL/Filter.thy	Fri Feb 19 13:40:50 2016 +0100
+++ b/src/HOL/Filter.thy	Mon Feb 22 14:37:56 2016 +0000
@@ -990,6 +990,9 @@
 translations
   "LIM x F1. f :> F2" == "CONST filterlim (\<lambda>x. f) F2 F1"
 
+lemma filterlim_top [simp]: "filterlim f top F"
+  by (simp add: filterlim_def)
+
 lemma filterlim_iff:
   "(LIM x F1. f x :> F2) \<longleftrightarrow> (\<forall>P. eventually P F2 \<longrightarrow> eventually (\<lambda>x. P (f x)) F1)"
   unfolding filterlim_def le_filter_def eventually_filtermap ..

--- a/src/HOL/Groups.thy	Fri Feb 19 13:40:50 2016 +0100
+++ b/src/HOL/Groups.thy	Mon Feb 22 14:37:56 2016 +0000
@@ -1203,6 +1203,16 @@
   thus "\<bar>a\<bar> \<le> 0" by simp
 qed
 
+lemma abs_le_self_iff [simp]: "\<bar>a\<bar> \<le> a \<longleftrightarrow> 0 \<le> a"
+proof -
+  have "\<forall>a. (0::'a) \<le> \<bar>a\<bar>"
+    using abs_ge_zero by blast
+  then have "\<bar>a\<bar> \<le> a \<Longrightarrow> 0 \<le> a"
+    using order.trans by blast
+  then show ?thesis
+    using abs_of_nonneg eq_refl by blast
+qed
+
 lemma zero_less_abs_iff [simp]: "0 < \<bar>a\<bar> \<longleftrightarrow> a \<noteq> 0"
 by (simp add: less_le)
 

--- a/src/HOL/Limits.thy	Fri Feb 19 13:40:50 2016 +0100
+++ b/src/HOL/Limits.thy	Mon Feb 22 14:37:56 2016 +0000
@@ -21,6 +21,14 @@
   by (subst eventually_INF_base)
      (auto simp: subset_eq eventually_principal intro!: exI[of _ "max a b" for a b])
 
+corollary eventually_at_infinity_pos:
+   "eventually p at_infinity \<longleftrightarrow> (\<exists>b. 0 < b \<and> (\<forall>x. norm x \<ge> b \<longrightarrow> p x))"
+apply (simp add: eventually_at_infinity, auto)
+apply (case_tac "b \<le> 0")
+using norm_ge_zero order_trans zero_less_one apply blast
+apply (force simp:)
+done
+
 lemma at_infinity_eq_at_top_bot:
   "(at_infinity :: real filter) = sup at_top at_bot"
   apply (simp add: filter_eq_iff eventually_sup eventually_at_infinity
@@ -67,14 +75,14 @@
   "Bfun f F \<longleftrightarrow> (\<exists>K>0. eventually (\<lambda>x. norm (f x) \<le> K) F)"
   unfolding Bfun_metric_def norm_conv_dist
 proof safe
-  fix y K assume "0 < K" and *: "eventually (\<lambda>x. dist (f x) y \<le> K) F"
+  fix y K assume K: "0 < K" and *: "eventually (\<lambda>x. dist (f x) y \<le> K) F"
   moreover have "eventually (\<lambda>x. dist (f x) 0 \<le> dist (f x) y + dist 0 y) F"
     by (intro always_eventually) (metis dist_commute dist_triangle)
   with * have "eventually (\<lambda>x. dist (f x) 0 \<le> K + dist 0 y) F"
     by eventually_elim auto
   with \<open>0 < K\<close> show "\<exists>K>0. eventually (\<lambda>x. dist (f x) 0 \<le> K) F"
     by (intro exI[of _ "K + dist 0 y"] add_pos_nonneg conjI zero_le_dist) auto
-qed auto
+qed (force simp del: norm_conv_dist [symmetric])
 
 lemma BfunI:
   assumes K: "eventually (\<lambda>x. norm (f x) \<le> K) F" shows "Bfun f F"
@@ -1036,10 +1044,9 @@
   proof eventually_elim
     fix x assume A: "dist (f x) c < 1/2" and B: "norm (f x) \<ge> norm c + 1"
     note B
-    also have "norm (f x) = dist (f x) 0" by (simp add: norm_conv_dist)
+    also have "norm (f x) = dist (f x) 0" by simp
     also have "... \<le> dist (f x) c + dist c 0" by (rule dist_triangle)
-    also note A
-    finally show False by (simp add: norm_conv_dist)
+    finally show False using A by simp
   qed
   with assms show False by simp
 qed
@@ -1541,6 +1548,11 @@
   shows "\<lbrakk>(f \<longlongrightarrow> a) F; ((\<lambda>x. f x - g x) \<longlongrightarrow> 0) F\<rbrakk> \<Longrightarrow> (g \<longlongrightarrow> a) F"
   by (erule Lim_transform) (simp add: tendsto_minus_cancel)
 
+proposition Lim_transform_eq:
+  fixes a :: "'a::real_normed_vector"
+  shows "((\<lambda>x. f x - g x) \<longlongrightarrow> 0) F \<Longrightarrow> (f \<longlongrightarrow> a) F \<longleftrightarrow> (g \<longlongrightarrow> a) F"
+using Lim_transform Lim_transform2 by blast
+
 lemma Lim_transform_eventually:
   "eventually (\<lambda>x. f x = g x) net \<Longrightarrow> (f \<longlongrightarrow> l) net \<Longrightarrow> (g \<longlongrightarrow> l) net"
   apply (rule topological_tendstoI)

--- a/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy	Fri Feb 19 13:40:50 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy	Mon Feb 22 14:37:56 2016 +0000
@@ -259,7 +259,7 @@
       by (rule dist_triangle_add)
     also have "\<dots> \<le> dist (Abs_bcontfun f) 0 + dist (Abs_bcontfun g) 0"
       unfolding zero_bcontfun_def using assms
-      by (auto intro!: add_mono dist_bounded_Abs const_bcontfun)
+      by (metis add_mono const_bcontfun dist_bounded_Abs)
     finally show "dist (f x + g x) 0 \<le> dist (Abs_bcontfun f) 0 + dist (Abs_bcontfun g) 0" .
   qed (simp add: continuous_on_add)
 qed
@@ -341,7 +341,7 @@
   fix f g :: "('a, 'b) bcontfun"
   show "dist f g = norm (f - g)"
     by (simp add: norm_bcontfun_def dist_bcontfun_def zero_bcontfun_def
-      Abs_bcontfun_inverse const_bcontfun norm_conv_dist[symmetric] dist_norm)
+      Abs_bcontfun_inverse const_bcontfun dist_norm)
   show "norm (f + g) \<le> norm f + norm g"
     unfolding norm_bcontfun_def
   proof (subst dist_bcontfun_def, safe intro!: cSUP_least)
@@ -364,31 +364,30 @@
     proof (intro continuous_at_Sup_mono bdd_aboveI2)
       fix x
       show "dist (Rep_bcontfun f x) 0 \<le> norm f" using dist_bounded[of f x 0]
-        by (simp add: norm_bcontfun_def norm_conv_dist Abs_bcontfun_inverse zero_bcontfun_def
+        by (simp add: norm_bcontfun_def Abs_bcontfun_inverse zero_bcontfun_def
           const_bcontfun)
     qed (auto intro!: monoI mult_left_mono continuous_intros)
     moreover
     have "range (\<lambda>x. dist (Rep_bcontfun (a *\<^sub>R f) x) 0) =
       (\<lambda>x. \<bar>a\<bar> * x) ` (range (\<lambda>x. dist (Rep_bcontfun f x) 0))"
-      by (auto simp: norm_conv_dist[symmetric])
+      by auto
     ultimately
     show "norm (a *\<^sub>R f) = \<bar>a\<bar> * norm f"
-      by (simp add: norm_bcontfun_def dist_bcontfun_def norm_conv_dist Abs_bcontfun_inverse
-        zero_bcontfun_def const_bcontfun image_image) presburger
+      by (simp add: norm_bcontfun_def dist_bcontfun_def Abs_bcontfun_inverse
+        zero_bcontfun_def const_bcontfun image_image)
   qed
 qed (auto simp: norm_bcontfun_def sgn_bcontfun_def)
 
 end
 
 lemma bcontfun_normI: "continuous_on UNIV f \<Longrightarrow> (\<And>x. norm (f x) \<le> b) \<Longrightarrow> f \<in> bcontfun"
-  unfolding norm_conv_dist
-  by (auto intro: bcontfunI)
+  by (metis bcontfunI dist_0_norm dist_commute)
 
 lemma norm_bounded:
   fixes f :: "('a::topological_space, 'b::real_normed_vector) bcontfun"
   shows "norm (Rep_bcontfun f x) \<le> norm f"
   using dist_bounded[of f x 0]
-  by (simp add: norm_bcontfun_def norm_conv_dist Abs_bcontfun_inverse zero_bcontfun_def
+  by (simp add: norm_bcontfun_def Abs_bcontfun_inverse zero_bcontfun_def
     const_bcontfun)
 
 lemma norm_bound:
@@ -396,8 +395,7 @@
   assumes "\<And>x. norm (Rep_bcontfun f x) \<le> b"
   shows "norm f \<le> b"
   using dist_bound[of f 0 b] assms
-  by (simp add: norm_bcontfun_def norm_conv_dist Abs_bcontfun_inverse zero_bcontfun_def
-    const_bcontfun)
+  by (simp add: norm_bcontfun_def Abs_bcontfun_inverse zero_bcontfun_def const_bcontfun)
 
 
 subsection \<open>Continuously Extended Functions\<close>

--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Fri Feb 19 13:40:50 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Mon Feb 22 14:37:56 2016 +0000
@@ -6489,7 +6489,7 @@
        if "z \<in> s" for z
   proof -
     obtain d h N where "0 < d" "summable h" and le_h: "\<And>n y. \<lbrakk>N \<le> n; y \<in> ball z d\<rbrakk> \<Longrightarrow> norm(f n y) \<le> h n"
-      using to_g \<open>z \<in> s\<close> by blast
+      using to_g \<open>z \<in> s\<close> by meson 
     then obtain r where "r>0" and r: "ball z r \<subseteq> ball z d \<inter> s" using \<open>z \<in> s\<close> s
       by (metis Int_iff open_ball centre_in_ball open_Int open_contains_ball_eq)
     have 1: "open (ball z d \<inter> s)"

--- a/src/HOL/Probability/Bochner_Integration.thy	Fri Feb 19 13:40:50 2016 +0100
+++ b/src/HOL/Probability/Bochner_Integration.thy	Mon Feb 22 14:37:56 2016 +0000
@@ -1229,7 +1229,7 @@
     s: "\<And>i. simple_function M (s i)" and
     pointwise: "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. s i x) \<longlonglongrightarrow> f x" and
     bound: "\<And>i x. x \<in> space M \<Longrightarrow> norm (s i x) \<le> 2 * norm (f x)"
-    by (simp add: norm_conv_dist) metis
+    by simp metis
   
   show ?thesis
   proof (rule integrableI_sequence)
@@ -2545,7 +2545,7 @@
   then have s: "\<And>i. simple_function (N \<Otimes>\<^sub>M M) (s i)"
     "\<And>x y. x \<in> space N \<Longrightarrow> y \<in> space M \<Longrightarrow> (\<lambda>i. s i (x, y)) \<longlonglongrightarrow> f x y"
     "\<And>i x y. x \<in> space N \<Longrightarrow> y \<in> space M \<Longrightarrow> norm (s i (x, y)) \<le> 2 * norm (f x y)"
-    by (auto simp: space_pair_measure norm_conv_dist)
+    by (auto simp: space_pair_measure)
 
   have [measurable]: "\<And>i. s i \<in> borel_measurable (N \<Otimes>\<^sub>M M)"
     by (rule borel_measurable_simple_function) fact

--- a/src/HOL/Product_Type.thy	Fri Feb 19 13:40:50 2016 +0100
+++ b/src/HOL/Product_Type.thy	Mon Feb 22 14:37:56 2016 +0000
@@ -1184,6 +1184,14 @@
   "snd ` (A \<times> B) = (if A = {} then {} else B)"
   by force
 
+lemma fst_image_Sigma:
+  "fst ` (Sigma A B) = {x \<in> A. B(x) \<noteq> {}}"
+  by force
+
+lemma snd_image_Sigma:
+  "snd ` (Sigma A B) = (\<Union> x \<in> A. B x)"
+  by force
+
 lemma vimage_fst:
   "fst -` A = A \<times> UNIV"
   by auto

--- a/src/HOL/Real_Vector_Spaces.thy	Fri Feb 19 13:40:50 2016 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy	Mon Feb 22 14:37:56 2016 +0000
@@ -862,6 +862,14 @@
   "norm (- numeral w::'a::real_normed_algebra_1) = numeral w"
 by (subst of_real_neg_numeral [symmetric], subst norm_of_real, simp)
 
+lemma norm_of_real_add1 [simp]:
+     "norm (of_real x + 1 :: 'a :: real_normed_div_algebra) = abs (x + 1)"
+  by (metis norm_of_real of_real_1 of_real_add)
+
+lemma norm_of_real_addn [simp]:
+     "norm (of_real x + numeral b :: 'a :: real_normed_div_algebra) = abs (x + numeral b)"
+  by (metis norm_of_real of_real_add of_real_numeral)
+
 lemma norm_of_int [simp]:
   "norm (of_int z::'a::real_normed_algebra_1) = \<bar>of_int z\<bar>"
 by (subst of_real_of_int_eq [symmetric], rule norm_of_real)
@@ -1298,6 +1306,8 @@
 lemma norm_conv_dist: "norm x = dist x 0"
   unfolding dist_norm by simp
 
+declare norm_conv_dist [symmetric, simp]
+
 lemma dist_diff [simp]: "dist a (a - b) = norm b"  "dist (a - b) a = norm b"
   by (simp_all add: dist_norm)
 
@@ -1868,7 +1878,7 @@
   have "inverse e < of_nat (nat \<lceil>inverse e + 1\<rceil>)" by linarith
   also note n
   finally show "dist (1 / of_nat n :: 'a) 0 < e" using e
-    by (simp add: divide_simps mult.commute norm_conv_dist[symmetric] norm_divide)
+    by (simp add: divide_simps mult.commute norm_divide)
 qed
 
 lemma (in metric_space) complete_def:

--- a/src/HOL/Series.thy	Fri Feb 19 13:40:50 2016 +0100
+++ b/src/HOL/Series.thy	Mon Feb 22 14:37:56 2016 +0000
@@ -390,6 +390,9 @@
     by (simp add: ac_simps)
 qed simp
 
+corollary sums_iff_shift': "(\<lambda>i. f (i + n)) sums (s - (\<Sum>i<n. f i)) \<longleftrightarrow> f sums s"
+  by (simp add: sums_iff_shift)
+
 lemma summable_iff_shift: "summable (\<lambda>n. f (n + k)) \<longleftrightarrow> summable f"
   by (metis diff_add_cancel summable_def sums_iff_shift[abs_def])
 
@@ -535,6 +538,12 @@
 lemma suminf_divide: "summable f \<Longrightarrow> suminf (\<lambda>n. f n / c) = suminf f / c"
   by (rule bounded_linear.suminf [OF bounded_linear_divide, symmetric])
 
+lemma sums_mult_D: "\<lbrakk>(\<lambda>n. c * f n) sums a; c \<noteq> 0\<rbrakk> \<Longrightarrow> f sums (a/c)"
+  using sums_mult_iff by fastforce
+
+lemma summable_mult_D: "\<lbrakk>summable (\<lambda>n. c * f n); c \<noteq> 0\<rbrakk> \<Longrightarrow> summable f"
+  by (auto dest: summable_divide)
+
 text\<open>Sum of a geometric progression.\<close>
 
 lemma geometric_sums: "norm c < 1 \<Longrightarrow> (\<lambda>n. c^n) sums (1 / (1 - c))"

--- a/src/HOL/Set_Interval.thy	Fri Feb 19 13:40:50 2016 +0100
+++ b/src/HOL/Set_Interval.thy	Mon Feb 22 14:37:56 2016 +0000
@@ -1640,6 +1640,11 @@
   finally show ?case .
 qed
 
+lemma setsum_atMost_shift:
+  fixes f :: "nat \<Rightarrow> 'a::comm_monoid_add"
+  shows "(\<Sum>i\<le>n. f i) = f 0 + (\<Sum>i<n. f (Suc i))"
+by (metis atLeast0AtMost atLeast0LessThan atLeastLessThanSuc_atLeastAtMost atLeastSucAtMost_greaterThanAtMost le0 setsum_head setsum_shift_bounds_Suc_ivl)
+
 lemma setsum_last_plus: fixes n::nat shows "m <= n \<Longrightarrow> (\<Sum>i = m..n. f i) = f n + (\<Sum>i = m..<n. f i)"
   by (cases n) (auto simp: atLeastLessThanSuc_atLeastAtMost add.commute)
 

--- a/src/HOL/Transcendental.thy	Fri Feb 19 13:40:50 2016 +0100
+++ b/src/HOL/Transcendental.thy	Mon Feb 22 14:37:56 2016 +0000
@@ -74,7 +74,7 @@
 
 subsection \<open>Properties of Power Series\<close>
 
-lemma powser_zero:
+lemma powser_zero [simp]:
   fixes f :: "nat \<Rightarrow> 'a::real_normed_algebra_1"
   shows "(\<Sum>n. f n * 0 ^ n) = f 0"
 proof -
@@ -89,6 +89,11 @@
     using sums_finite [of "{0}" "\<lambda>n. a n * 0 ^ n"]
     by simp
 
+lemma powser_sums_zero_iff [simp]:
+  fixes a :: "nat \<Rightarrow> 'a::real_normed_div_algebra"
+  shows "(\<lambda>n. a n * 0^n) sums x \<longleftrightarrow> a 0 = x"
+using powser_sums_zero sums_unique2 by blast
+
 text\<open>Power series has a circle or radius of convergence: if it sums for @{term
   x}, then it sums absolutely for @{term z} with @{term "\<bar>z\<bar> < \<bar>x\<bar>"}.\<close>
 
@@ -1342,6 +1347,31 @@
 lemma exp_setsum: "finite I \<Longrightarrow> exp(setsum f I) = setprod (\<lambda>x. exp(f x)) I"
   by (induction I rule: finite_induct) (auto simp: exp_add_commuting mult.commute)
 
+lemma exp_divide_power_eq:
+  fixes x:: "'a::{real_normed_field,banach}"
+  assumes "n>0" shows "exp (x / of_nat n) ^ n = exp x"
+using assms
+proof (induction n arbitrary: x)
+  case 0 then show ?case by simp
+next
+  case (Suc n)
+  show ?case
+  proof (cases "n=0")
+    case True then show ?thesis by simp
+  next
+    case False
+    then have [simp]: "x * of_nat n / (1 + of_nat n) / of_nat n = x / (1 + of_nat n)"
+      by simp
+    have [simp]: "x / (1 + of_nat n) + x * of_nat n / (1 + of_nat n) = x"
+      apply (simp add: divide_simps)
+      using of_nat_eq_0_iff apply (fastforce simp: distrib_left)
+      done
+    show ?thesis
+      using Suc.IH [of "x * of_nat n / (1 + of_nat n)"] False
+      by (simp add: exp_add [symmetric])
+  qed
+qed
+
 
 subsubsection \<open>Properties of the Exponential Function on Reals\<close>