Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Analysis/ex/Approximations.thy
changeset 72222 01397b6e5eb0
parent 70817 dd675800469d 
--- a/src/HOL/Analysis/ex/Approximations.thy	Thu Aug 27 16:48:21 2020 +0100
+++ b/src/HOL/Analysis/ex/Approximations.thy	Fri Aug 28 12:04:36 2020 +0100
@@ -99,9 +99,8 @@
   from assms show "(exp x - approx) \<ge> 0"
     by (intro sums_le[OF _ sums_zero sums]) auto
 
-  have "\<forall>k. x^n * (x^k / fact (n+k)) \<le> (x^n / fact n) * (x / 2)^k"
-  proof
-    fix k :: nat
+  have "x^n * (x^k / fact (n+k)) \<le> (x^n / fact n) * (x / 2)^k" for k::nat
+  proof -
     have "x^n * (x^k / fact (n + k)) = x^(n+k) / fact (n + k)" by (simp add: power_add)
     also from assms have "\<dots> \<le> x^(n+k) / (2^k * fact n)"
       by (intro divide_left_mono two_power_fact_le_fact zero_le_power) simp_all
isabelle