diff -r 209c4cbbc4cd -r 6c731c8b7f03 src/HOL/Multivariate_Analysis/Gamma.thy
--- a/src/HOL/Multivariate_Analysis/Gamma.thy	Sat Jul 02 15:02:24 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Gamma.thy	Sat Jul 02 20:22:25 2016 +0200
@@ -512,9 +512,10 @@
     by (intro setprod.cong[OF refl], subst exp_Ln) (auto simp: field_simps plus_of_nat_eq_0_imp)
   also have "... = (\<Prod>k=1..n. z + k) / fact n" unfolding fact_altdef
     by (subst setprod_dividef [symmetric]) (simp_all add: field_simps)
-  also from assms have "z * ... = (\<Prod>k=0..n. z + k) / fact n"
+  also from assms have "z * ... = (\<Prod>k\<le>n. z + k) / fact n"
     by (cases n) (simp_all add: setprod_nat_ivl_1_Suc)
-  also have "(\<Prod>k=0..n. z + k) = pochhammer z (Suc n)" unfolding pochhammer_def by simp
+  also have "(\<Prod>k\<le>n. z + k) = pochhammer z (Suc n)" unfolding pochhammer_def
+    by (simp add: lessThan_Suc_atMost)
   also have "of_nat n powr z / (pochhammer z (Suc n) / fact n) = Gamma_series z n"
     unfolding Gamma_series_def using assms by (simp add: divide_simps powr_def Ln_of_nat)
   finally show ?thesis .
@@ -999,7 +1000,7 @@
   hence "z \<noteq> - of_nat n" for n by auto
   from rGamma_series_aux[OF this] show ?thesis
     by (simp add: rGamma_series_def[abs_def] fact_altdef pochhammer_Suc_setprod
-                  exp_def of_real_def[symmetric] suminf_def sums_def[abs_def])
+                  exp_def of_real_def[symmetric] suminf_def sums_def[abs_def] atLeast0AtMost)
 qed (insert rGamma_eq_zero_iff[of z], simp_all add: rGamma_series_nonpos_Ints_LIMSEQ)
 
 lemma Gamma_series_LIMSEQ [tendsto_intros]:
@@ -1364,7 +1365,7 @@
             pochhammer' = \<lambda>a n. \<Prod>n = 0..n. a + of_nat n
         in  (\<lambda>n. pochhammer' z n / (fact' n * exp (z * ln (real_of_nat n) *\<^sub>R 1))) \<longlonglongrightarrow> rGamma z"
     by (simp add: fact_altdef pochhammer_Suc_setprod rGamma_series_def [abs_def] exp_def
-                  of_real_def [symmetric] suminf_def sums_def [abs_def])
+                  of_real_def [symmetric] suminf_def sums_def [abs_def] atLeast0AtMost)
 qed
 
 end
@@ -1497,7 +1498,7 @@
             pochhammer' = \<lambda>a n. \<Prod>n = 0..n. a + of_nat n
         in  (\<lambda>n. pochhammer' x n / (fact' n * exp (x * ln (real_of_nat n) *\<^sub>R 1))) \<longlonglongrightarrow> rGamma x"
     by (simp add: fact_altdef pochhammer_Suc_setprod rGamma_series_def [abs_def] exp_def
-                  of_real_def [symmetric] suminf_def sums_def [abs_def])
+                  of_real_def [symmetric] suminf_def sums_def [abs_def] atLeast0AtMost)
 qed
 
 end
@@ -2424,7 +2425,7 @@
                         setprod_inversef[symmetric] divide_inverse)
     also have "(\<Prod>k=1..n. (1 + z / of_nat k)) = pochhammer (z + 1) n / fact n"
       by (cases n) (simp_all add: pochhammer_def fact_altdef setprod_shift_bounds_cl_Suc_ivl
-                                  setprod_dividef[symmetric] divide_simps add_ac)
+                                  setprod_dividef[symmetric] divide_simps add_ac atLeast0AtMost lessThan_Suc_atMost)
     also have "z * \<dots> = pochhammer z (Suc n) / fact n" by (simp add: pochhammer_rec)
     finally show "?r n = Gamma_series_euler' z n / Gamma_series z n" by simp
   qed