diff --git a/thys/Irrationality_J_Hancl/Irrationality_J_Hancl.thy b/thys/Irrationality_J_Hancl/Irrationality_J_Hancl.thy
--- a/thys/Irrationality_J_Hancl/Irrationality_J_Hancl.thy
+++ b/thys/Irrationality_J_Hancl/Irrationality_J_Hancl.thy
@@ -1,1005 +1,1005 @@
 (*
   File: Irrationality_J_Hancl.thy
   Authors:  Angeliki Koutsoukou-Argyraki and Wenda Li,
             Computer Laboratory, University of Cambridge, UK.
   Email: ak2110@cam.ac.uk, wl302@cam.ac.uk  
 *)
 
 section \<open>Irrational Rapidly Convergent Series\<close>
 theory Irrationality_J_Hancl
   imports "HOL-Analysis.Analysis" "HOL-Decision_Procs.Approximation"
 begin
 
-text \<open>This is the formalisation of a proof by J. Hancl, in particular of the proof of his Theorem 3 in
+text \<open>This is the formalisation of a proof by J. Hančl, in particular of the proof of his Theorem 3 in
 the paper: Irrational Rapidly Convergent Series, Rend. Sem. Mat. Univ. Padova, Vol 107 (2002).
 
 The statement asserts the irrationality of the sum of a series consisting of rational numbers
 defined using sequences that fulfill certain properties. Even though the statement
 is number-theoretic, the proof uses only arguments from introductory Analysis.\<close>
 
-text \<open>We show the central result (theorem Hancl3) by proof by contradiction, by making use of some of 
+text \<open>We prove the central result (theorem Hancl3) by contradiction, by making use of some of 
  the auxiliary lemmas. To this end, assuming that the sum is a rational number, for a quantity 
  $\textrm{ALPHA}(n)$ we show that $\textrm{ALPHA}(n) \geq 1$ for all $n \in \mathbb{N}$. After that we show that we can find an 
   $n \in \mathbb{N}$ for which $\textrm{ALPHA}(n) < 1$ which yields a contradiction and we thus conclude that the 
-  sum of the series is a rational number. We finally give an immediate application of theorem Hancl3
+  sum of the series is rational. We finally give an immediate application of theorem Hancl3
  for a specific series (corollary Hancl3corollary, requiring lemma
  summable\_ln\_plus) which corresponds to Corollary 2 in the original
-paper by J. Hancl. 
+paper by J. Hančl. 
 \<close>
 
 hide_const floatarith.Max
 
 subsection \<open>Misc\<close>
 
 lemma filterlim_sequentially_iff:
   "filterlim f F1 sequentially \<longleftrightarrow> filterlim (\<lambda>x. f (x+k)) F1 sequentially"
   unfolding filterlim_iff
   by (metis eventually_at_top_linorder eventually_sequentially_seg)
 
 lemma filterlim_realpow_sequentially_at_top:
   "(x::real) > 1 \<Longrightarrow> filterlim (power x) at_top sequentially"
   apply (rule LIMSEQ_divide_realpow_zero[THEN filterlim_inverse_at_top,of _ 1,simplified])
   by auto
 
 lemma filterlim_at_top_powr_real:
   fixes g::"'b \<Rightarrow> real"
   assumes "filterlim f at_top F" "(g \<longlongrightarrow> g') F" "g'>1"
   shows "LIM x F. g x powr f x :> at_top"
 proof -
   have "LIM x F. ((g' + 1) / 2) powr f x :> at_top" 
   proof (subst filterlim_at_top_gt[of _ _ 1],rule+)
-    fix Z assume "Z>(1::real)"
+    fix Z::real assume "Z > 1"
     have "\<forall>\<^sub>F x in F. ln Z / ln ((g' + 1) / 2) \<le> f x"
       using assms(1) filterlim_at_top by blast
     then have "\<forall>\<^sub>F x in F. ln Z \<le> ln (((g' + 1) / 2) powr f x)"
     proof (eventually_elim)
       case (elim x)
       then show ?case
       using \<open>g'>1\<close> by (auto simp:ln_powr divide_simps)        
     qed
     then show "\<forall>\<^sub>F x in F. Z \<le> ((g' + 1) / 2) powr f x"
     proof (eventually_elim)
       case (elim x)
       then show ?case
         using \<open>1 < Z\<close> \<open>g'>1\<close> by auto
     qed
   qed
   moreover have "\<forall>\<^sub>F x in F. ((g'+1)/2) powr f x \<le> g x powr f x" 
   proof -
     have "\<forall>\<^sub>F x in F. g x > (g'+1)/2"
       apply (rule order_tendstoD[OF assms(2)])
       using \<open>g'>1\<close> by auto
     moreover have "\<forall>\<^sub>F x in F. f x>0"
       using assms(1) filterlim_at_top_dense by blast 
     ultimately show ?thesis
     proof eventually_elim
       case (elim x)
       then show ?case
         using \<open>g'>1\<close> by (auto intro!: powr_mono2)
     qed
   qed
   ultimately show ?thesis using filterlim_at_top_mono by fast
 qed
 
 lemma powrfinitesum:
   fixes a::real and s::nat assumes  "s \<le> n"
   shows " (\<Prod>j=s..(n::nat).(a powr (2^j)))  = a powr (\<Sum>j=s..(n::nat).(2^j)) "
   using \<open>s \<le> n\<close> 
 proof(induct n)
   case 0
   then show ?case by auto
 next
   case (Suc n)
   have ?case when "s\<le>n" using Suc.hyps 
     by (metis Suc.prems add.commute linorder_not_le powr_add prod.nat_ivl_Suc' sum.cl_ivl_Suc that)
   moreover have ?case when "s=Suc n"   
   proof-
     have "(\<Prod>j = s..Suc n. a powr 2 ^ j) =(a powr 2 ^(Suc n))  " 
       using \<open>s=Suc n\<close> by simp
     also have "a powr 2 ^ Suc n = a powr sum (power 2) {s..Suc n}" using that by auto
     ultimately show "(\<Prod>j = s..Suc n. a powr 2 ^ j) = a powr sum (power 2) {s..Suc n}"
       using \<open>s\<le>Suc n\<close> by linarith
   qed
   ultimately show ?case using \<open>s\<le>Suc n\<close> by linarith
 qed
 
 lemma summable_ratio_test_tendsto:
   fixes f :: "nat \<Rightarrow> 'a::banach"
   assumes "c < 1" and "\<forall>n. f n\<noteq>0" and "(\<lambda>n. norm (f (Suc n)) / norm (f n)) \<longlonglongrightarrow> c"
   shows "summable f"
 proof -
   obtain N where N_dist:"\<forall>n\<ge>N. dist (norm (f (Suc n)) / norm (f n)) c < (1-c)/2"
     using assms unfolding tendsto_iff eventually_sequentially 
     by (meson diff_gt_0_iff_gt zero_less_divide_iff zero_less_numeral)
   have "norm (f (Suc n)) / norm (f n) \<le> (1+c)/2" when "n\<ge>N" for n
     using N_dist[rule_format,OF that] \<open>c<1\<close> 
     apply (auto simp add:field_simps dist_norm)
     by argo
   then have "norm (f (Suc n))  \<le> (1+c)/2 * norm (f n)" when "n\<ge>N" for n
     using that assms(2)[rule_format, of n] by (auto simp add:divide_simps)
   moreover have "(1+c)/2 < 1" using \<open>c<1\<close> by auto 
   ultimately show ?thesis
     using summable_ratio_test[of _ N f] by blast
 qed
 
 lemma summable_ln_plus:
   fixes f::"nat \<Rightarrow> real" 
   assumes "summable f" "\<forall>n. f n>0"
   shows "summable (\<lambda>n. ln (1+f n))"
 proof (rule summable_comparison_test_ev[OF _ assms(1)])
   have "ln (1 + f n) > 0" for n by (simp add: assms(2) ln_gt_zero)
   moreover have "ln (1 + f n) \<le> f n" for n 
     apply (rule ln_add_one_self_le_self2)
     using assms(2)[rule_format,of n] by auto 
   ultimately show "\<forall>\<^sub>F n in sequentially. norm (ln (1 + f n)) \<le> f n"
     by (auto intro!: eventuallyI simp add:less_imp_le) 
 qed
 
 lemma suminf_real_offset_le:
   fixes f :: "nat \<Rightarrow> real"
   assumes f: "\<And>i. 0 \<le> f i" and "summable f"
   shows "(\<Sum>i. f (i + k)) \<le> suminf f"
 proof -
   have "(\<lambda>n. \<Sum>i<n. f (i + k)) \<longlonglongrightarrow> (\<Sum>i. f (i + k))"
     using summable_sums[OF \<open>summable f\<close>] 
     by (simp add: assms(2) summable_LIMSEQ summable_ignore_initial_segment)
   moreover have "(\<lambda>n. \<Sum>i<n. f i) \<longlonglongrightarrow> (\<Sum>i. f i)"
     using summable_sums[OF \<open>summable f\<close>] by (simp add: sums_def atLeast0LessThan f)
   then have "(\<lambda>n. \<Sum>i<n + k. f i) \<longlonglongrightarrow> (\<Sum>i. f i)"
     by (rule LIMSEQ_ignore_initial_segment)
   ultimately show ?thesis
   proof (rule LIMSEQ_le, safe intro!: exI[of _ k])
     fix n assume "k \<le> n"
     have "(\<Sum>i<n. f (i + k)) = (\<Sum>i<n. (f \<circ> (\<lambda>i. i + k)) i)"
       by simp
     also have "\<dots> = (\<Sum>i\<in>(\<lambda>i. i + k) ` {..<n}. f i)"
       by (subst sum.reindex) auto
     also have "\<dots> \<le> sum f {..<n + k}"
       by (intro sum_mono2) (auto simp: f)
     finally show "(\<Sum>i<n. f (i + k)) \<le> sum f {..<n + k}" .
   qed
 qed
 
 
 
 lemma factt:
   fixes s n ::nat assumes "s \<le> n" 
   shows " (\<Sum>i=s..n. 2^i) < (2^(n+1) :: real) " using assms
 proof (induct n)
   case 0
   show ?case by  auto 
 next
   case (Suc n)
   have ?case when  "s=n+1" using that by auto
   moreover have ?case when  "s \<noteq> n+1" 
   proof -
     have"(\<Sum>i=s..(n+1). 2^i ) = (\<Sum>i=s..n. 2^i ) + (2::real)^(n+1) "
       using sum.cl_ivl_Suc \<open>s \<le> Suc n \<close>
       by (auto simp add:add.commute)
     also have "... < (2) ^ (n +1) + (2)^(n+1)" 
     proof -
       have "s \<le>n" using that  \<open>s \<le> Suc n \<close> by auto
       then show ?thesis
         using Suc.hyps \<open>s \<le> n\<close> by linarith
     qed
     also have "... = 2^(n+2)" by simp
     finally show "(\<Sum>i=s..(Suc n). 2^i )< (2::real)^(Suc n+1)" by auto
   qed
   ultimately show ?case by blast
 qed
 
 subsection \<open>Auxiliary lemmas and the main proof\<close>
 
 lemma showpre7:
   fixes a b ::"nat\<Rightarrow>int " and q p::int
   assumes "q>0" and "p>0"and a: "\<forall>n. a n>0" and "\<forall>n. b n>0" and 
     assumerational:"(\<lambda> n. b (n+1) / a (n+1) )  sums (p/q)"
   shows "q*((\<Prod>j=1..n. of_int( a j)))*(suminf (\<lambda>(j::nat). (b (j+n+1)/ a (j+n+1 )))) 
         = ((\<Prod>j=1..n. of_int( a j)))*(p -q* (\<Sum>j=1..n. b j / a j))       " 
 proof -
   define aa where "aa=(\<Prod>j = 1..n. real_of_int (a j))"
   define ff where "ff=(\<lambda>i. real_of_int (b (i+1)) / real_of_int (a (i+1)))"
 
   have "(\<Sum>j. ff (j+n)) =  (\<Sum>n. ff n) - sum ff {..<n}"
     apply (rule suminf_minus_initial_segment)
     using assumerational unfolding ff_def by (simp add: sums_summable)
   also have "... = p/q - sum ff {..<n}"
     using assumerational unfolding ff_def by (simp add: sums_iff)
   also have "... = p/q - (\<Sum>j=1..n. ff (j-1))"
   proof -
     have "sum ff {..<n} = (\<Sum>j=1..n. ff (j-1))"
       apply (subst sum_bounds_lt_plus1[symmetric])
       by simp
     then show ?thesis unfolding ff_def by auto
   qed
   finally have "(\<Sum>j. ff (j + n)) = p / q - (\<Sum>j = 1..n. ff (j - 1))" .
   then have "q*(\<Sum>j. ff (j + n)) = p - q*(\<Sum>j = 1..n. ff (j - 1))"
     using \<open>q>0\<close> by (auto simp add:field_simps)
   then have "aa*q*(\<Sum>j. ff (j + n)) = aa*(p - q*(\<Sum>j = 1..n. ff (j - 1)))" 
     by auto
   then show ?thesis unfolding aa_def ff_def by auto
 qed
 
 lemma show7:
   fixes d::"nat\<Rightarrow>real" and a b::"nat\<Rightarrow>int " and q p::int
   assumes "q \<ge>1" and "p \<ge> 1" and a: "\<forall>n. a n \<ge> 1" and "\<forall>n. b n \<ge> 1"
     and assumerational:"(\<lambda> n. b (n+1) / a (n+1) ) sums (p/q)"
   shows "q*((\<Prod>j=1..n. of_int( a j)))*( suminf (\<lambda> (j::nat). (b (j+n+1)/ a (j+n+1 )))) \<ge> 1 "
     (is "?L \<ge> _")
 proof-
   define LL where "LL=?L"
   define aa where "aa=(\<Prod>j = 1..n. real_of_int (a j))"
   define ff where "ff=(\<lambda>i. real_of_int (b (i+1)) / real_of_int (a (i+1)))"
 
   have "?L > 0"
   proof -
     have "aa > 0"
       unfolding aa_def using a
     by (induction n) (simp_all add: int_one_le_iff_zero_less prod_pos)
     moreover have "(\<Sum>j. ff (j + n)) > 0"
     proof (rule suminf_pos)
       have "summable ff" unfolding ff_def using assumerational
         using summable_def by blast
       then show " summable (\<lambda>j. ff (j + n))" using summable_iff_shift[of ff n] by auto
       show "\<And>i. 0 < ff (i + n)" unfolding ff_def using a assms(4) int_one_le_iff_zero_less by auto
     qed
     ultimately show ?thesis unfolding aa_def ff_def using \<open>q\<ge>1\<close> by auto
   qed
   moreover have "?L \<in> \<int>"
   proof -
     have "?L = aa *(p -q* ( \<Sum>j=1..n. b j / a j))"
       unfolding aa_def
       using a assms assumerational int_one_le_iff_zero_less showpre7 by force
     also have "... = aa * p - q * (\<Sum>j=1..n. aa * b j / a j)"
       by (auto simp add:algebra_simps sum_distrib_left)
     also have "... = prod a {1..n} * p - q * (\<Sum>j = 1..n. b j * prod a ({1..n} - {j}))"
     proof -
       have "(\<Sum>j=1..n. aa * b j / a j) = (\<Sum>j=1..n. b j * prod a ({1..n} - {j}))"
         unfolding of_int_sum
       proof (rule sum.cong)
         fix j assume "j \<in> {1..n}"
         then have "(\<Prod>i = 1..n. real_of_int (a i)) = a j * (\<Prod>i\<in>{1..n} - {j}. real_of_int (a i))"
           by (meson finite_atLeastAtMost prod.remove)
         then have "aa / real_of_int (a j) = prod a ({1..n} - {j})"
           unfolding aa_def using a[rule_format,of j] by (auto simp add:field_simps)
         then show "aa * b j / a j = b j * prod a ({1..n} - {j})"
           by (metis mult.commute of_int_mult times_divide_eq_right)
       qed simp
       moreover have "aa * p = (\<Prod>j = 1..n.  (a j)) *  p"
         unfolding aa_def by auto
       ultimately show ?thesis by force
     qed
     also have "... \<in> \<int>" using Ints_of_int by blast
     finally show ?thesis .
   qed
   ultimately show ?thesis 
     apply (fold LL_def)
     by (metis Ints_cases int_one_le_iff_zero_less not_less of_int_0_less_iff of_int_less_1_iff)
 qed
 
 lemma show8:
   fixes d ::"nat\<Rightarrow>real " and a :: "nat\<Rightarrow>int" and s k::nat 
   assumes "A > 1" and d: "\<forall>n. d n> 1"  and a:"\<forall>n. a n>0" and "s>0"
     and "convergent_prod d"
     and assu2: "\<forall>n \<ge> s. A / of_int (a n) powr (1 / of_int (2^n)) > (\<Prod>j. d (n + j))"
   shows "\<forall>n\<ge>s. (\<Prod>j. d (j+n)) < A / (MAX j\<in>{s..n}. of_int (a j) powr (1 / of_int (2 ^ j)))"
 proof (intro strip)
   fix n assume "s \<le> n"
   define sp where "sp \<equiv> (\<lambda>n. \<Prod>j. d (j+n))"
   define ff where "ff \<equiv> (\<lambda>(j::nat). (real_of_int (a j)) powr(1 /of_int (2^j)))"
   have "sp i \<ge> sp n" when "i\<le>n" for i
   proof -
     have "(\<Prod>j. d (j + i)) = (\<Prod>ia. d (ia + (n - i) + i)) * (\<Prod>ia<n - i. d (ia + i))"
     proof (rule prodinf_split_initial_segment) 
       show "convergent_prod (\<lambda>j. d (j + i))"
         using \<open>convergent_prod d\<close> convergent_prod_iff_shift[of d i] by simp
       show "\<And>j. j < n - i \<Longrightarrow> d (j + i) \<noteq> 0"
         by (metis d not_one_less_zero)
     qed
     then have "sp i = sp n * (\<Prod>j<n - i. d (i + j))"
       unfolding sp_def using \<open>n\<ge>i\<close> by (auto simp:algebra_simps)
     moreover have "sp i>1" "sp n>1" 
       unfolding sp_def using convergent_prod_iff_shift \<open>convergent_prod d\<close> d 
       by (auto intro!:less_1_prodinf)
     moreover have "(\<Prod>j<n - i. d (i + j)) \<ge> 1" 
       using d less_imp_le by (auto intro: prod_ge_1)
     ultimately show ?thesis by auto
   qed
   moreover have "\<forall>j\<ge>s. A / ff j > sp j" 
     unfolding ff_def sp_def using assu2 by (auto simp:algebra_simps)
   ultimately have "\<forall>j. s\<le>j \<and> j\<le>n \<longrightarrow> A / ff j > sp n" by force
   then show "sp n< A / Max (ff ` {s..n})" 
     by (metis (mono_tags, hide_lams) Max_in \<open>n\<ge>s\<close> atLeastAtMost_iff empty_iff 
         finite_atLeastAtMost finite_imageI imageE image_is_empty order_refl)
 qed
 
 lemma auxiliary1_9:
   fixes d ::"nat\<Rightarrow>real" and a::"nat\<Rightarrow>int " and s m::nat 
   assumes d: "\<forall>n. d n> 1"  and a: "\<forall>n. a n>0" and "s>0" and "n \<ge> m" and " m \<ge> s"
     and auxifalse_assu: "\<forall>n\<ge>m. (of_int (a (n+1))) powr(1 /of_int (2^(n+1))) <
               (d (n+1))* (Max ((\<lambda> (j::nat). (of_int (a j)) powr(1 /of_int (2^j))) ` {s..n} ))"
   shows "(of_int (a (n+1))) powr(1 /of_int (2^(n+1))) <
     (\<Prod>j=(m+1)..(n+1). d j) * (Max ((\<lambda> (j::nat). (of_int (a j)) powr(1 /of_int (2^j))) ` {s..m}))"
 proof-
   define ff where "ff \<equiv> \<lambda>j. real_of_int (a j) powr (1 / of_int (2^j))"
   have [simp]:"ff j > 0" for j
     unfolding ff_def by (metis a less_numeral_extra(3) of_int_0_less_iff powr_gt_zero)
 
   have ff_asm:"ff (n+1) < d (n+1) * Max (ff ` {s..n})" when "n\<ge>m" for n
     using auxifalse_assu that unfolding ff_def by simp
   from \<open>n\<ge>m\<close>
   have Q: "(Max( ff ` {s..n} )) \<le> (\<Prod>j=(m+1)..n. d j)* (Max (ff ` {s..m}))"
   proof(induct n)
     case 0
     then show ?case using \<open>m\<ge>s\<close> by simp 
   next
     case (Suc n)
     have ?case when "m=Suc n"
       using that by auto
     moreover have ?case when "m\<noteq>Suc n" 
     proof -
       have "m \<le> n" using that Suc(2) by simp
       then have IH: "Max (ff ` {s..n}) \<le> prod d {m + 1..n} * Max (ff ` {s..m})"
         using Suc(1) by linarith
       have "Max (ff ` {s..Suc n}) = Max (ff ` {s..n} \<union> {ff (Suc n)})"
         using Suc.prems assms(5) atLeastAtMostSuc_conv by auto
       also have "... = max (Max (ff ` {s..n})) (ff (Suc n))"
         using Suc.prems assms(5) max_def sup_assoc that by auto
       also have "... \<le> max (Max (ff ` {s..n})) (d (n+1) * Max (ff ` {s..n}))"
         using \<open>m \<le> n\<close> ff_asm by fastforce
       also have "... \<le> Max (ff ` {s..n}) * max 1 (d (n+1))"
       proof -
         have "Max (ff ` {s..n}) \<ge> 0" 
           by (metis (mono_tags, hide_lams) Max_in \<open>\<And>j. 0 < ff j\<close> \<open>m \<le> n\<close> assms(5) 
               atLeastAtMost_iff empty_iff finite_atLeastAtMost finite_imageI imageE 
               image_is_empty less_eq_real_def)
         then show ?thesis using max_mult_distrib_right 
           by (simp add: max_mult_distrib_right mult.commute)
       qed
       also have "... = Max (ff ` {s..n}) * d (n+1)"
         by (metis d max.commute max.strict_order_iff)
       also have "... \<le>  prod d {m + 1..n} * Max (ff ` {s..m}) * d (n+1)"
         using IH d[rule_format, of "n+1"] by auto
       also have "... = prod d {m + 1..n+1} * Max (ff ` {s..m})"
         using \<open>n\<ge>m\<close> by (simp add:prod.nat_ivl_Suc' algebra_simps)
       finally show ?case by simp
     qed
     ultimately show ?case by blast
   qed
   then have "d (n+1) * Max (ff ` {s..n} ) \<le> (\<Prod>j=(m+1)..(n+1). d j)* (Max (ff ` {s..m}))"
     using \<open>m\<le>n\<close> d[rule_format,of "Suc n"] by (simp add:prod.nat_ivl_Suc')
   then show ?thesis using ff_asm[of n] \<open>s\<le>m\<close> \<open>m\<le>n\<close> unfolding ff_def by auto
 qed
 
 lemma show9:
   fixes d ::"nat\<Rightarrow>real " and a :: "nat\<Rightarrow>int " and s ::nat and A::real
   assumes   "A > 1" and  d: "\<forall>n. d n> 1"  and a: "\<forall>n. a n>0" and "s>0"  
     and assu1: "(( \<lambda> n. (of_int (a n)) powr(1 /of_int (2^n)))\<longlongrightarrow> A) sequentially "
     and "convergent_prod d"
     and 8: "\<forall>n\<ge>s. prodinf (\<lambda>j. d( n+j)) 
                   < A/(Max ((\<lambda>(j::nat). (of_int (a j)) powr(1 /of_int (2^j))) ` {s..n})) "
   shows "\<forall>m \<ge>s. \<exists>n\<ge>m.  ( (of_int (a (n+1))) powr(1 /of_int (2^(n+1))) \<ge>
           (d (n+1))* (Max ( ( \<lambda> (j::nat). (of_int (a j)) powr(1 /of_int (2^j))) ` {s..n} )))"
 proof (rule ccontr)
   define ff where "ff \<equiv> (\<lambda>j. real_of_int (a j) powr (1 / of_int (2^j)))"
   assume assumptioncontra: " \<not> (\<forall>m \<ge>s. \<exists>n\<ge>m. ff(n+1) \<ge> d(n+1) * Max (ff  ` {s..n}))"
 
   then obtain t where "t\<ge>s" and
     ttt: "\<forall>n\<ge>t. ff (n+1) < d (n+1) * Max (ff ` {s..n})"               
     by fastforce
   define B where "B \<equiv> \<Prod>j. d (t + 1 + j)"
   have "B>0" unfolding B_def 
   proof (rule less_0_prodinf)
     show "convergent_prod (\<lambda>j. d (t + 1 + j))"
       using convergent_prod_iff_shift[of d "t+1"] \<open>convergent_prod d\<close> 
       by (auto simp: algebra_simps)
     show "\<And>i. 0 < d (t + 1 + i)"
       using d le_less_trans zero_le_one by blast
   qed
   have "A \<le> B * Max ( ff ` {s..t})"
   proof (rule tendsto_le[of sequentially "\<lambda>n. (\<Prod>j=(t+1)..(n+1). d j) * Max ( ff ` {s..t})" _ 
         "\<lambda>n. ff (n+1)"])
     show "(\<lambda>n. ff (n + 1)) \<longlonglongrightarrow> A"
       using assu1[folded ff_def] LIMSEQ_ignore_initial_segment by blast
     have "(\<lambda>n. prod d {t + 1..n + 1}) \<longlonglongrightarrow> B"
     proof -
       have "convergent_prod (\<lambda>j. d (t + 1 + j))"
         using \<open>convergent_prod d\<close> convergent_prod_iff_shift[of d "t+1"] by (simp add:algebra_simps)
       then have "(\<lambda>n. \<Prod>i\<le>n. d (t + 1 + i)) \<longlonglongrightarrow> B"
         using B_def convergent_prod_LIMSEQ by blast
       then have "(\<lambda>n. \<Prod>i\<in>{0..n}. d (i+(t + 1))) \<longlonglongrightarrow> B"
         using atLeast0AtMost by (auto simp:algebra_simps)
       then have "(\<lambda>n. prod d {(t + 1)..n + (t + 1)}) \<longlonglongrightarrow> B" 
         apply (subst (asm) prod.shift_bounds_cl_nat_ivl[symmetric])
         by simp
       from seq_offset_neg[OF this,of "t"]
       show "(\<lambda>n. prod d {t + 1..n+1}) \<longlonglongrightarrow> B"
         apply (elim Lim_transform)
         apply (rule LIMSEQ_I)
         apply (rule exI[where x="t+1"])
         by auto
     qed
     then show "(\<lambda>n. prod d {t + 1..n + 1} * Max (ff ` {s..t})) \<longlonglongrightarrow> B * Max (ff ` {s..t})" 
       by (auto intro:tendsto_eq_intros)
     have "\<forall>\<^sub>F n in sequentially. (ff (n+1)) < (\<Prod>j=(t+1)..(n+1). d j) * (Max ( ff ` {s..t}))"
       unfolding eventually_sequentially ff_def
       using auxiliary1_9[OF d a \<open>s>0\<close> _ \<open>t\<ge>s\<close> ttt[unfolded ff_def]]
       by blast
     then show "\<forall>\<^sub>F n in sequentially. (ff (n+1)) \<le> (\<Prod>j=(t+1)..(n+1). d j) * (Max ( ff ` {s..t}))"
       by (eventually_elim,simp)
   qed simp
   also have "... \<le> B * Max ( ff ` {s..t+1})"
   proof -
     have "Max (ff ` {s..t}) \<le> Max (ff ` {s..t + 1})"
       using \<open>t\<ge>s\<close> by (auto intro: Max_mono)
     then show ?thesis using \<open>B>0\<close> by auto
   qed
   finally have "A \<le> B * Max (ff ` {s..t + 1})" 
     unfolding B_def .
   moreover have "B < A / Max (ff ` {s..t + 1})"
     using 8[rule_format, of "t+1",folded ff_def B_def] \<open>s\<le>t\<close> by auto
   moreover have "Max (ff ` {s..t+1})>0"
     using \<open>A \<le> B * Max (ff ` {s..t + 1})\<close> \<open>B>0\<close> \<open>A>1\<close> zero_less_mult_pos [of B "Max (ff ` {s..Suc t})"]
     by fastforce
   ultimately show False by (auto simp add:field_simps)
 qed
 
 lemma show10:
   fixes d ::"nat\<Rightarrow>real " and  a ::"nat\<Rightarrow>int " and s::nat
   assumes d [rule_format]: "\<forall>n. d n> 1" 
     and a [rule_format]: "\<forall>n. a n>0"  and " s>0"
     and 9: "\<forall>m \<ge>s. \<exists>n\<ge>m. a (n+1) powr(1 / of_int (2^(n+1))) \<ge>
           d (n+1) * (Max ((\<lambda>j. (of_int (a j)) powr(1 /of_int (2^j))) ` {s..n} ))"
   shows "\<forall>m\<ge>s. \<exists>n\<ge>m. d (n+1) powr(2^(n+1)) * (\<Prod>j=1..n. of_int( a j)) * 
             (1 / (\<Prod>j=1..s-1. of_int( a j))) \<le> a (n+1)"
 proof (intro strip)
   fix m assume "s \<le> m" 
   from 9[rule_format,OF this]
   obtain n where "n\<ge>m" and asm_9:"( (of_int (a (n+1))) powr(1 /of_int (2^(n+1))) \<ge>
           (d (n+1))* (Max ( ( \<lambda> (j::nat). (of_int (a j)) powr(1 /of_int (2^j))) ` {s..n} )))"
     by auto
   with \<open>s\<le>m\<close> have "s\<le>n" by auto
 
   define M where "M \<equiv> \<lambda>s. MAX j\<in>{s..n}. a j powr (1 / real_of_int (2 ^ j))"
   have prod: "(\<Prod>j=1..n. real_of_int (a j)) * (1 / (\<Prod>j=1..s-1. of_int(a j)))
             = (\<Prod>j=s..n. of_int( a j))"
   proof -
     define f where "f= (\<lambda>j. real_of_int( a j))"
     have "{Suc 0..n}= {Suc 0..s - Suc 0} \<union> {s..n}" using \<open>n\<ge>s\<close>  \<open>s >0\<close>
       by auto
     then have "(\<Prod>j=1..n. f j) = (\<Prod>j=1..s-1. f j) * (\<Prod>j=s..n. f j)"
       apply (subst prod.union_disjoint[symmetric])
       by auto
     moreover have "(\<Prod>j=1..s-1. f j) > 0 "
       by (metis a f_def of_int_0_less_iff prod_pos)
     then have "(\<Prod>j=1..s-1. f j) \<noteq> 0" by argo
     ultimately show ?thesis unfolding f_def by auto 
   qed
   then have "d (n+1) powr 2 ^ (n+1) * (\<Prod>j = 1..n. of_int (a j)) * (1 / (\<Prod>j = 1..s - 1. of_int (a j))) =
              d (n+1) powr 2 ^ (n+1) * (\<Prod>j = s..n. of_int (a j))" 
      by (metis mult.assoc prod)
   also have
     "... \<le> ((d (n+1))powr(2^(n+1) ) * (\<Prod>i=s..n. M s powr(2^i)) )"
   proof (rule mult_left_mono)
     show "0 \<le> (d (n + 1)) powr 2 ^ (n + 1)"
       by auto
     show "(\<Prod>j = s..n. real_of_int (a j)) \<le> (\<Prod>i = s..n. M s powr 2 ^ i)"
     proof (intro prod_mono conjI)
       fix i assume i: "i \<in> {s..n}"
       have "a i = (a i powr (1 / real_of_int (2 ^ i))) powr 2 ^ i"
         unfolding powr_powr by (simp add: a less_eq_real_def)
       also have  "\<dots> \<le> M s powr(2^i)" 
         unfolding M_def using i by (force intro: powr_mono2)
       finally show "a i \<le> M s powr 2 ^ i" .
       show "\<And>i. i \<in> {s..n} \<Longrightarrow> 0 \<le> real_of_int (a i)"
         by (meson a less_imp_le of_int_0_le_iff)
     qed
   qed
   also have "... = d(n+1) powr (2^(n+1)) * M s powr (\<Sum>i=s..n. 2^i)"
   proof-
     have  "d (n+1) powr (2^(n+1)) \<ge> 1  "
       by (metis Transcendental.log_one d le_powr_iff zero_le_numeral zero_le_power zero_less_one)
     moreover have "(\<Prod>i=s..n. M s powr(2^i)) = M s powr (\<Sum>i=s..n. 2^i ) "
       using \<open>s\<le>n\<close> powrfinitesum by auto
     ultimately show ?thesis by auto
   qed
   also have "... \<le> d (n + 1) powr 2 ^ (n + 1) * M s powr(2^(n+1))"
   proof -
     have "sum (power 2) {s..n} < (2::real) ^ (n + 1)" using factt \<open>s\<le>n\<close> by auto
     moreover have "1 \<le> M s" 
     proof -
       define S where "S=(\<lambda>(j::nat). ( of_int( a j) powr(1 /real_of_int (2^j)) )) ` {s..n  }"
       have "finite S" unfolding S_def by auto
       moreover have "S\<noteq>{}" unfolding S_def using \<open>s\<le>n\<close>  by auto
       moreover have "\<exists>x\<in>S. x\<ge>1"
       proof-
         have "a s powr (1 / (2^s)) \<ge> 1"  
         proof (rule ge_one_powr_ge_zero)
           show "1 \<le> real_of_int (a s)"
             by (simp add: a int_one_le_iff_zero_less)
         qed auto
         moreover have "of_int( a s) powr(1 /real_of_int (2^s)) \<in> S" 
           unfolding S_def
           using \<open>s\<le>n\<close> by auto
         ultimately show ?thesis by auto
       qed
       ultimately show ?thesis 
         using Max_ge_iff[of S 1] unfolding S_def M_def by blast
     qed
     moreover have "0 \<le> (d (n + 1)) powr 2 ^ (n + 1)" by auto
     ultimately show ?thesis
       by (simp add: mult_left_mono powr_mono M_def)
   qed
 
   also have "... =  (d (n+1) * M s) powr(2^(n+1))"
   proof -
     have "d (n + 1) \<ge> 0" using d[of "n+1"] by argo
     moreover have "M s \<ge> 0"
       using \<open>s\<le>n\<close> by (auto simp: M_def Max_ge_iff)
     ultimately show ?thesis 
       unfolding M_def using powr_mult by auto
   qed
   also have "... \<le> (real_of_int (a (n + 1)) powr (1 / real_of_int (2 ^ (n + 1)))) powr 2 ^ (n + 1)"
   proof (rule powr_mono2)
     have "M s \<ge> 0"
       using \<open>s\<le>n\<close> by (auto simp: M_def Max_ge_iff)
     moreover have "d (n + 1) \<ge>0" 
       using d[of "n+1"] by argo
     ultimately show "0 \<le> (d (n + 1)) * M s" by auto
     show "(d (n + 1)) * M s \<le> real_of_int (a (n + 1)) powr (1 / real_of_int (2 ^ (n + 1)))"
       using M_def asm_9 by presburger
   qed simp    
   also have "... =  (of_int (a (n+1)))" 
     by (simp add: a less_eq_real_def pos_add_strict powr_powr)
   finally show "\<exists>n\<ge>m. d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)) *
                 (1 / (\<Prod>j = 1..s - 1. real_of_int (a j)))
                 \<le> real_of_int (a (n + 1))" using \<open>n\<ge>m\<close> \<open>m\<ge>s\<close> 
     by force
 qed
 
 lemma lasttoshow:
   fixes d ::"nat\<Rightarrow>real " and a b ::"nat\<Rightarrow>int " and q::int and s::nat
   assumes d: "\<forall>n. d n> 1"
      and a:"\<forall>n. a n>0" and "s>0" and "q>0"  
     and "A > 1" and b:"\<forall>n. b n>0" and 9:
     "\<forall>m\<ge>s. \<exists>n\<ge>m. ((of_int (a (n+1))) powr(1 /of_int (2^(n+1))) \<ge>
           (d (n+1))* (Max ((\<lambda>(j::nat). (of_int (a j)) powr(1 /of_int (2^j))) ` {s..n} )))"
     and assu3: "filterlim( \<lambda> n. (d n)^(2^n)/ b n) at_top sequentially "
     and 5: "\<forall>\<^sub>F n in sequentially. (\<Sum>j. (b (n + j)) /  (a (n + j))) \<le> 2 * b n / a n"
   shows "\<exists>n. q*((\<Prod>j=1..n. real_of_int(a j))) * suminf (\<lambda>(j::nat). (b (j+n+1)/ a (j+n+1)))<1"
 proof-
   define as where "as=(\<Prod>j = 1..s - 1. real_of_int (a j))"
   obtain n where "n\<ge>s" and n_def1:"real_of_int q * as * 2 
       * real_of_int (b (n + 1)) / d (n + 1) powr 2 ^ (n + 1) < 1"
     and n_def2:"d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)) * (1 / as) 
           \<le> real_of_int (a (n + 1))"
     and n_def3:"(\<Sum>j. (b (n+1 + j)) /  (a (n+1 + j))) \<le> 2 * b (n+1) / a (n+1)"
   proof -
     have *:"(\<lambda>n. real_of_int (b n) / d n ^ 2 ^ n) \<longlonglongrightarrow> 0"
       using tendsto_inverse_0_at_top[OF assu3] by auto
     then have "(\<lambda>n. real_of_int (b n) / d n powr 2 ^ n) \<longlonglongrightarrow> 0"
     proof -
       have "d n ^ 2 ^ n = d n powr (of_nat (2 ^ n))" for n
         by (metis d le_less_trans powr_realpow zero_le_one) 
       then show ?thesis using * by auto
     qed
     from tendsto_mult_right_zero[OF this,of "q * as * 2"] 
     have "(\<lambda>n. q * as * 2 * b n / d n powr 2 ^ n) \<longlonglongrightarrow> 0"
       by auto
     then have "\<forall>\<^sub>F n in sequentially. q * as * 2 * b n / d n powr 2 ^ n < 1"
       by (elim order_tendstoD) simp
     then have "\<forall>\<^sub>F n in sequentially. q * as * 2 * b n / d n powr 2 ^ n < 1 
                   \<and> (\<Sum>j. (b (n + j)) /  (a (n + j))) \<le> 2 * b n / a n"
       using 5 by eventually_elim auto
     then obtain N where N_def:"\<forall>n\<ge>N. q * as * 2 * b n / d n powr 2 ^ n < 1 
             \<and> (\<Sum>j. (b (n + j)) /  (a (n + j))) \<le> 2 * b n / a n"
       unfolding eventually_sequentially by auto
     obtain n where "n\<ge>s" and "n\<ge>N" and n_def:"d (n + 1) powr 2 ^ (n + 1) 
                 * (\<Prod>j = 1..n. of_int (a j)) * (1 / as) \<le> real_of_int (a (n + 1))"
       using show10[OF d a \<open>s>0\<close> 9,folded as_def,rule_format,of "max s N"] by auto
     with N_def[rule_format, of "n+1"] that[of n]  show ?thesis by auto
   qed
 
   define pa where "pa \<equiv> (\<Prod>j = 1..n. real_of_int (a j))"
   define dn where "dn \<equiv> d (n + 1) powr 2 ^ (n + 1)"
   have [simp]:"dn >0" "as > 0" 
     subgoal unfolding dn_def by (metis d not_le numeral_One powr_gt_zero zero_le_numeral)
     subgoal unfolding as_def by (simp add: a prod_pos)
     done
   have [simp]:"pa>0"
     unfolding pa_def using a by (simp add: prod_pos)
 
   have K: "q* (\<Prod>j=1..n. real_of_int (a j)) * suminf (\<lambda> (j::nat). (b (j+n+1)/ a (j+n+1)))
               \<le>q* (\<Prod>j=1..n. real_of_int (a j)) *2* (b (n+1))/(a( n+1))"
     apply (fold pa_def)
     using mult_left_mono[OF n_def3,of "real_of_int q * pa"] 
       \<open>n\<ge>s\<close> \<open>pa>0\<close> \<open>q>0\<close> by (auto simp add:algebra_simps) 
   also have KK:"... \<le> 2*q* (\<Prod>j=1..n. real_of_int (a j)) * (b(n+1))*
       ((\<Prod>j=1..s-1. real_of_int( a j))/((d (n+1))powr(2^(n+1)) * (\<Prod>j=1..n. real_of_int ( a j))))" 
   proof -
     have " dn * pa * (1 / as) \<le> real_of_int (a (n + 1))"
       using n_def2 unfolding dn_def pa_def .
     then show ?thesis 
       apply (fold pa_def dn_def as_def)
       using \<open>pa>0\<close> \<open>q>0\<close> a[rule_format, of "Suc n"] b[rule_format, of "Suc n"]
       by (auto simp add: field_simps)
   qed
   also have KKK: "... = q * (\<Prod>j=1..(s-1). real_of_int(a j)) * 2 * b (n+1) / d (n+1) powr 2^(n+1)"
     apply (fold as_def pa_def dn_def)
     apply simp
     using \<open>0 < pa\<close> by blast
   also have KKKK: "... < 1" using n_def1 unfolding as_def by simp
   finally show ?thesis by auto
 qed
 
 lemma 
   fixes d ::"nat\<Rightarrow>real " and  a b ::"nat\<Rightarrow>int " and A::real
   assumes "A > 1" and d: "\<forall>n. d n> 1" and a: "\<forall>n. a n>0" and b:"\<forall>n. b n>0" 
     and assu1: "(( \<lambda> n. (of_int (a n)) powr(1 /of_int (2^n)))\<longlongrightarrow> A) sequentially "
     and assu3: "filterlim ( \<lambda> n. (d n)^(2^n)/ b n) at_top sequentially"
     and "convergent_prod d"
   shows issummable: "summable (\<lambda>j. b j / a j)"
     and show5: "\<forall>\<^sub>F n in sequentially. (\<Sum>j. (b (n + j)) / (a (n + j))) \<le> 2 * b n / a n"
 proof-
   define c where "c = (\<lambda>j. b j / a j)"
   have c_pos:"c j>0" for j 
     using a b unfolding c_def by simp
   have c_ratio_tendsto:"(\<lambda>n. c (n+1) / c n ) \<longlonglongrightarrow> 0"
   proof -
     define nn where "nn \<equiv> (\<lambda>n. (2::int) ^ (Suc n))"
     define ff where "ff \<equiv> (\<lambda>n. (a n / a (Suc n)) powr(1 /nn n)*(d(Suc n)))"
     have nn_pos:"nn n>0" and ff_pos:"ff n>0" for n
       subgoal unfolding nn_def by simp
       subgoal unfolding ff_def
         using d[rule_format, of "Suc n"] a[rule_format, of n] a[rule_format, of "Suc n"]
         by auto
       done
     have ff_tendsto:"ff \<longlonglongrightarrow> 1 / sqrt A" 
     proof -
       have "(of_int (a n)) powr(1 / (nn n)) = sqrt(of_int (a n) powr(1 /of_int (2^n)))" for n
         unfolding nn_def using a
         by (simp add: powr_half_sqrt [symmetric] powr_powr ac_simps)
       moreover have "(( \<lambda> n. sqrt(of_int (a n) powr(1 /of_int (2^n))))\<longlongrightarrow> sqrt A) sequentially " 
         using assu1 tendsto_real_sqrt by blast
       ultimately have "(( \<lambda> n. (of_int (a n)) powr(1 /of_int (nn n)))\<longlongrightarrow> sqrt A) sequentially " 
         by auto
       from tendsto_divide[OF this assu1[THEN LIMSEQ_ignore_initial_segment[where k=1]]] 
       have "(\<lambda>n. (a n / a (Suc n)) powr(1 /nn n)) \<longlonglongrightarrow> 1/sqrt A"
         using \<open>A>1\<close> a unfolding nn_def
         by (auto simp add:powr_divide less_imp_le inverse_eq_divide sqrt_divide_self_eq)
       moreover have "(\<lambda>n. d (Suc n))\<longlonglongrightarrow> 1" 
         apply (rule convergent_prod_imp_LIMSEQ)
         using convergent_prod_iff_shift[of d 1] \<open>convergent_prod d\<close> by auto
       ultimately show ?thesis
         unfolding ff_def by (auto intro:tendsto_eq_intros)
     qed
     have "(\<lambda>n. (ff n) powr nn n) \<longlonglongrightarrow> 0" 
     proof -
       define aa where "aa=(1+1/sqrt A) / 2"
       have "eventually (\<lambda>n. ff n<aa) sequentially"
         apply (rule order_tendstoD[OF ff_tendsto])
         unfolding aa_def using \<open>A>1\<close> by (auto simp add:field_simps)
       moreover have "(\<lambda>n. aa powr nn n) \<longlonglongrightarrow> 0" 
       proof -
         have "(\<lambda>y. aa ^ (nat \<circ> nn) y) \<longlonglongrightarrow> 0"
           apply (rule tendsto_power_zero)
           subgoal unfolding nn_def comp_def
             apply (rule filterlim_subseq)
             by (auto intro:strict_monoI)
           subgoal unfolding aa_def using \<open>A>1\<close> by auto
           done
         then show ?thesis
         proof (elim filterlim_mono_eventually)
           have "aa>0" unfolding aa_def using \<open>A>1\<close> 
             by  (auto simp add:field_simps pos_add_strict)
           then show " \<forall>\<^sub>F x in sequentially. aa ^ (nat \<circ> nn) x = aa powr real_of_int (nn x)"
             by (auto simp: powr_int order.strict_implies_order[OF nn_pos])
         qed auto
       qed
       ultimately show ?thesis
         apply (elim metric_tendsto_imp_tendsto)
         apply (auto intro!:powr_mono2 elim!:eventually_mono)
         using nn_pos ff_pos by (meson le_cases not_le)+
     qed
     then have "(\<lambda>n. (d (Suc n))^(nat (nn n)) * (a n / a (Suc n))) \<longlonglongrightarrow> 0" 
     proof (elim filterlim_mono_eventually)
       show "\<forall>\<^sub>F x in sequentially. ff x powr  (nn x) = d (Suc x) ^ nat (nn x) * (a x / a (Suc x))" 
         apply (rule eventuallyI)
         subgoal for x
           unfolding ff_def
           using a[rule_format,of x] a[rule_format,of "Suc x"] d[rule_format,of "Suc x"] nn_pos[of x]
           apply (auto simp add:field_simps powr_divide powr_powr powr_mult )
           by (simp add: powr_int)
         done
     qed auto 
     moreover have "(\<lambda>n. b (Suc n) / (d (Suc n))^(nat (nn n))) \<longlonglongrightarrow> 0"
       using tendsto_inverse_0_at_top[OF assu3,THEN LIMSEQ_ignore_initial_segment[where k=1]]
       unfolding nn_def by (auto simp add:field_simps nat_mult_distrib nat_power_eq)
     ultimately have "(\<lambda>n. b (Suc n) * (a n / a (Suc n))) \<longlonglongrightarrow> 0" 
       apply -
       subgoal premises asm
         using tendsto_mult[OF asm,simplified]
         apply (elim filterlim_mono_eventually)
         using d by (auto simp add:algebra_simps,metis (mono_tags, lifting) always_eventually 
             not_one_less_zero)
       done
     then have "(\<lambda>n. (b (Suc n) / b n) * (a n / a (Suc n))) \<longlonglongrightarrow> 0" 
       apply (elim Lim_transform_bound[rotated])
       apply (rule eventuallyI)
       subgoal for x using a[rule_format, of x] a[rule_format, of "Suc x"] 
           b[rule_format, of x] b[rule_format, of "Suc x"]
         by (auto simp add:field_simps)
       done
     then show ?thesis unfolding c_def by (auto simp add:algebra_simps)
   qed
   from c_ratio_tendsto
   have "(\<lambda>n. norm (b (Suc n) / a (Suc n)) / norm (b n / a n)) \<longlonglongrightarrow> 0" 
     unfolding c_def
     using a b by (force simp add:divide_simps abs_of_pos intro: Lim_transform_eventually)
   from summable_ratio_test_tendsto[OF _ _ this] a b 
   show "summable c" unfolding c_def
     by (metis c_def c_pos less_irrefl zero_less_one)
   have "\<forall>\<^sub>F n in sequentially. (\<Sum>j. c (n + j)) \<le> 2 * c n"
   proof -
     obtain N where N_ratio:"\<forall>n\<ge>N. c (n + 1) / c n < 1 / 2" 
     proof -
       have "eventually (\<lambda>n. c (n+1) / c n < 1/2) sequentially" 
         using c_ratio_tendsto[unfolded tendsto_iff,rule_format, of "1/2",simplified]
         apply eventually_elim
         subgoal for n using c_pos[of n] c_pos[of "Suc n"] by auto
         done
       then show ?thesis using that unfolding eventually_sequentially by auto
     qed
     have "(\<Sum>j. c (j + n)) \<le> 2 * c n" when "n\<ge>N" for n
     proof -
       have "(\<Sum>j<m. c (j + n)) \<le> 2*c n * (1 - 1 / 2^(m+1))" for m
       proof (induct m)
         case 0
         then show ?case using c_pos[of n] by simp
       next
         case (Suc m)
         have "(\<Sum>j<Suc m. c (j + n)) = c n + (\<Sum>i<m. c (Suc i + n)) "
           unfolding sum.lessThan_Suc_shift by simp
         also have "... \<le> c n + (\<Sum>i<m. c (i + n) / 2)"
         proof -
           have "c (Suc i + n) \<le> c (i + n) / 2" for i
             using N_ratio[rule_format,of "i+n"] \<open>n\<ge>N\<close> c_pos[of "i+n"]  by simp
           then show ?thesis by (auto intro:sum_mono)
         qed
         also have "... = c n + (\<Sum>i<m. c (i + n)) / 2"
           unfolding sum_divide_distrib by simp
         also have "... \<le> c n + c n * (1 - 1 / 2 ^ (m + 1))"
           using Suc by auto
         also have "... = 2 * c n * (1 - 1 / 2 ^ (Suc m + 1))"
           by (auto simp add:field_simps)
         finally show ?case .
       qed
       then have "(\<Sum>j<m. c (j + n)) \<le> 2*c n" for m
         using c_pos[of n] 
         by (smt divide_le_eq_1_pos divide_pos_pos nonzero_mult_div_cancel_left zero_less_power)
       moreover have "summable (\<lambda>j. c (j + n))" 
         using \<open>summable c\<close> by (simp add: summable_iff_shift)
       ultimately show ?thesis using suminf_le_const[of "\<lambda>j. c (j+n)" "2*c n"] by auto
     qed
     then show ?thesis unfolding eventually_sequentially by (auto simp add:algebra_simps)
   qed
   then show "\<forall>\<^sub>F n in sequentially. (\<Sum>j. (b (n + j)) /  (a (n + j))) \<le> 2 * b n / a n"
     unfolding c_def by simp
 qed
 
 
 theorem Hancl3:
   fixes d ::"nat\<Rightarrow>real" and  a b :: "nat\<Rightarrow>int"
   assumes "A > 1" and d: "\<forall>n. d n > 1" and a: "\<forall>n. a n>0" and b: "\<forall>n. b n > 0" and "s>0"
     and assu1: "(\<lambda>n. (a n) powr(1 / of_int(2^n))) \<longlonglongrightarrow> A"
     and assu2: "\<forall>n \<ge> s. A / (a n) powr (1 / of_int(2^n)) > (\<Prod>j. d (n+j))"
     and assu3: "LIM n sequentially. d n ^ 2 ^ n / b n :> at_top"
     and "convergent_prod d" 
   shows "(\<Sum>n. b n / a n) \<notin> \<rat>"
 proof (rule ccontr)
   assume asm: "\<not> ((\<Sum>n. b n / a n) \<notin> \<rat>)"
   have ab_sum: "summable (\<lambda>j. b j / a j)"
     using issummable[OF \<open>A>1\<close> d a b assu1 assu3 \<open>convergent_prod d\<close>] .
   obtain p q ::int where "q>0" and pq_def: "(\<lambda>n. b (n+1) / a (n+1)) sums (p/q)"
   proof -
     from asm have "(\<Sum>n. b n / a n) \<in> \<rat>" by auto
     then have "(\<Sum>n. b (n+1) / a (n+1)) \<in> \<rat>" 
       apply (subst suminf_minus_initial_segment[OF ab_sum,of 1])
       by auto   
     then obtain p' q' ::int where "q'\<noteq>0" and pq_def: "(\<lambda> n. b (n+1) / a (n+1) ) sums (p'/q')"
       unfolding Rats_eq_int_div_int
       using summable_ignore_initial_segment[OF ab_sum,of 1,THEN summable_sums]
       by force
     define p q where "p \<equiv> (if q'<0 then -p' else p')" and "q \<equiv> (if q'<0 then -q' else q')"
     have "p'/q' = p/q" "q>0" 
       using \<open>q'\<noteq>0\<close> unfolding p_def q_def by auto
     then show ?thesis using that[of q p] pq_def by auto
   qed
 
   define ALPHA where 
     "ALPHA = (\<lambda>n. of_int q * (\<Prod>j=1..n. of_int(a j)) * (\<Sum>j. (b (j+n+1)/a (j+n+1))))"
   have "ALPHA n \<ge> 1" for n 
   proof -
     have "(\<Sum>n. b (n+1) / a (n+1)) > 0"
     proof (rule suminf_pos)
       show "summable (\<lambda>n. b (n + 1) / real_of_int (a (n + 1)))"
         using summable_ignore_initial_segment[OF ab_sum,of 1] by auto
       show "\<And>n. 0 < b (n + 1) / a (n + 1)"
         using a b by simp
     qed
     then have "p/q > 0"
       using pq_def sums_unique by force
     then have "q\<ge>1" "p\<ge>1" using \<open>q>0\<close> by (auto simp add:divide_simps)
     moreover have "\<forall>n. 1 \<le> a n" "\<forall>n. 1 \<le> b n" using a b 
       by (auto simp add: int_one_le_iff_zero_less)
     ultimately show ?thesis unfolding ALPHA_def
       using show7[OF _ _ _ _ pq_def] by auto
   qed
   moreover have "\<exists>n. ALPHA n < 1" unfolding ALPHA_def
   proof (rule lasttoshow[OF d a \<open>s>0\<close> \<open>q>0\<close> \<open>A>1\<close> b _ assu3])
     show "\<forall>\<^sub>F n in sequentially. (\<Sum>j. b (n+j) / a (n+j)) \<le> (2 * b n) / a n"
       using show5[OF \<open>A>1\<close> d a b assu1 assu3 \<open>convergent_prod d\<close>] by simp
     show "\<forall>m\<ge>s. \<exists>n\<ge>m. d (n+1) * (MAX j\<in>{s..n}. a j powr (1 / of_int (2 ^ j)))
                     \<le> a (n+1) powr (1 / of_int (2 ^ (n+1)))"
       apply (rule show9[OF \<open>A>1\<close> d a \<open>s>0\<close> assu1 \<open>convergent_prod d\<close>])
       using show8[OF \<open>A>1\<close> d a \<open>s>0\<close> \<open>convergent_prod d\<close> assu2] by (simp add:algebra_simps)
   qed
   ultimately show False using not_le by blast
 qed
 
 corollary Hancl3corollary:
   fixes A::real and  a b :: "nat\<Rightarrow>int"
   assumes "A > 1" and a: "\<forall>n. a n>0" and b: "\<forall>n. b n>0"
     and assu1: "(\<lambda>n. (a n) powr(1 / of_int(2^n))) \<longlonglongrightarrow> A"
     and asscor2: "\<forall>n \<ge> 6. a n powr(1 / of_int (2^n)) * (1 + 4*(2/3)^n) \<le> A
                         \<and> b n \<le> 2 powr (4/3)^(n-1)"
   shows "(\<Sum>n. b n / a n) \<notin> \<rat>"
 proof-
   define d::"nat\<Rightarrow>real" where "d= (\<lambda> n. 1+(2/3)^(n+1))" 
   have dgt1:"\<forall>n. 1 < d n " unfolding d_def by auto
   moreover have "convergent_prod d"
     unfolding d_def
     by (simp add: abs_convergent_prod_imp_convergent_prod summable_imp_abs_convergent_prod)
   moreover have "\<forall>n\<ge>6. (\<Prod>j. d (n+j)) < A / a n powr (1 / of_int (2 ^ n))"
   proof (intro strip)
     fix n::nat assume "6 \<le> n"
     have d_sum:"summable (\<lambda>j. ln (d j))" unfolding d_def
       by (auto intro: summable_ln_plus)
 
     have "(\<Sum>j. ln (d (n + j))) < ln (1+4 * (2/3) ^ n)"
     proof -
       define c::real where "c = (2/3) ^ n"
       have "0<c" "c<1/8" 
       proof -
         have "c = (2/3)^6 * (2/3) ^ (n-6)"
           unfolding c_def using \<open>n\<ge>6\<close>
           by (metis le_add_diff_inverse power_add)
         also have "... \<le> (2/3)^6" by (auto intro:power_le_one)
         also have "... < 1/8" by (auto simp add:field_simps)
         finally show "c < 1/8" .
       qed (simp add:c_def)
 
       have "(\<Sum>j. ln (d (n + j))) \<le> (\<Sum>j. (2/3) ^ (n + j + 1))"
       proof (rule suminf_le)
         show "\<And>j. ln (d (n + j)) \<le> (2/3) ^ (n + j + 1)"
           unfolding d_def
           by (metis divide_pos_pos less_eq_real_def ln_add_one_self_le_self zero_less_numeral zero_less_power)
         show "summable (\<lambda>j. ln (d (n + j)))"
           using summable_ignore_initial_segment[OF d_sum] 
           by (force simp add: algebra_simps)
         show "summable (\<lambda>j. (2 / 3::real) ^ (n + j + 1))"
           using summable_geometric[THEN summable_ignore_initial_segment,of "2/3" "n+1"]
           by (auto simp add:algebra_simps)
       qed
       also have "... = (\<Sum>j. (2/3)^(n+1)*(2/3) ^ j)"
         by (auto simp add:algebra_simps power_add)
       also have "... = (2/3)^(n+1) * (\<Sum>j. (2/3) ^ j)"
         by (force intro!: summable_geometric suminf_mult)
       also have "... = 2 * c"
         unfolding c_def
         by (simp add: suminf_geometric)
       also have "... <  4 * c - (4 * c)\<^sup>2"
         using \<open>0<c\<close> \<open>c<1/8\<close>
         by (sos "((((A<0 * A<1) * R<1) + ((A<=0 * R<1) * (R<1/16 * [1]^2))))")
       also have "... \<le> ln (1 + 4 * c)"
         apply (rule ln_one_plus_pos_lower_bound)
         using \<open>0<c\<close> \<open>c<1/8\<close> by auto
       finally show ?thesis unfolding c_def by simp
     qed
     then have "exp (\<Sum>j. ln (d (n + j))) < 1 + 4 * (2/3) ^ n"
       by (smt (z3) divide_pos_pos ln_exp ln_ge_iff zero_less_power)
     moreover have "exp (\<Sum>j. ln (d (n + j))) = (\<Prod>j. d (n + j))"
     proof (subst exp_suminf_prodinf_real [symmetric])
       show "\<And>k. 0 \<le> ln (d (n + k))" 
         using dgt1 by (simp add: less_imp_le)
       show "abs_convergent_prod (\<lambda>na. exp (ln (d (n + na))))"
       proof (subst exp_ln)
         show "\<And>j. 0 < d (n + j)"
           using dgt1 le_less_trans zero_le_one by blast
         show "abs_convergent_prod (\<lambda>j. d (n + j))"
           unfolding abs_convergent_prod_def 
           using \<open>convergent_prod d\<close> 
           by (simp add: dgt1 convergent_prod_iff_shift less_imp_le algebra_simps)
       qed
       show "(\<Prod>j. exp (ln (d (n + j)))) = (\<Prod>j. d (n + j))"
         by (meson dgt1 exp_ln not_less not_one_less_zero order_trans)
     qed
     ultimately have "(\<Prod>j. d (n + j))  < 1 + 4 * (2/3) ^ n"
       by simp
     also have "... \<le> A / (a n) powr (1 / of_int (2 ^ n))" 
     proof -
       have "a n powr (1 / real_of_int (2 ^ n)) > 0"
         using a[rule_format,of n] by auto
       then show ?thesis using asscor2[rule_format,OF \<open>6\<le>n\<close>] 
         by (auto simp add:field_simps)
     qed
     finally show "(\<Prod>j. d (n + j)) < A / real_of_int (a n) powr (1 / of_int (2 ^ n))" .
   qed
   moreover have "LIM n sequentially. d n ^ 2 ^ n / real_of_int (b n) :> at_top" 
   proof -
     have "LIM n sequentially. d n ^ 2 ^ n / 2 powr((4/3)^(n-1)) :> at_top"
     proof -
       define n1 where "n1 \<equiv> (\<lambda>n. (2::real) * (3/2)^(n-1))"
       define n2 where "n2 \<equiv> (\<lambda>n. ((4::real)/3)^(n-1))"
       have "LIM n sequentially. (((1+(8/9)/(n1 n)) powr (n1 n))/2) powr (n2 n) :> at_top" 
       proof (rule filterlim_at_top_powr_real[where g'="exp (8/9) / 2"])
         define e1 where "e1 = exp (8/9) / (2::real)"
         show "e1>1" unfolding e1_def by (approximation 4)
         show "(\<lambda>n. ((1+(8/9)/(n1 n)) powr (n1 n))/2) \<longlonglongrightarrow> e1"
         proof -
           have "(\<lambda>n. (1+(8/9)/(n1 n)) powr (n1 n)) \<longlonglongrightarrow> exp (8/9)"
             apply (rule filterlim_compose[OF tendsto_exp_limit_at_top])
             unfolding n1_def
             by (auto intro!: filterlim_tendsto_pos_mult_at_top 
                 filterlim_realpow_sequentially_at_top
                 simp:filterlim_sequentially_iff[of "\<lambda>x. (3 / 2) ^ (x - Suc 0)" _ 1])
           then show ?thesis unfolding e1_def
             by (intro tendsto_intros,auto)
         qed
         show "filterlim n2 at_top sequentially"
           unfolding n2_def
           apply (subst filterlim_sequentially_iff[of "\<lambda>n. (4 / 3) ^ (n - 1)" _ 1])
           by (auto intro:filterlim_realpow_sequentially_at_top)
       qed
       moreover have "\<forall>\<^sub>F n in sequentially. (((1+(8/9)/(n1 n)) powr (n1 n))/2) powr (n2 n)
         = d n ^ 2 ^ n / 2 powr((4/3)^(n-1))"
       proof (rule eventually_sequentiallyI)
         fix k::nat assume "k \<ge> 1"
         have "((1 + 8 / 9 / n1 k) powr n1 k / 2) powr n2 k 
             = (((1 + 8 / 9 / n1 k) powr n1 k) powr n2 k) / 2 powr (4 / 3) ^ (k - 1)"
           by (simp add: n1_def n2_def powr_divide)
         also have "... = (1 + 8 / 9 / n1 k) powr (n1 k * n2 k) / 2 powr (4 / 3) ^ (k - 1)"
           by (simp add: powr_powr)
         also have "... = (1 + 8 / 9 / n1 k) powr (2 ^ k) / 2 powr (4 / 3) ^ (k - 1)"
         proof -
           have "n1 k * n2 k = 2 ^ k" 
             unfolding n1_def n2_def
             using \<open>k\<ge>1\<close> by (simp add: mult_ac flip:power_mult_distrib power_Suc)
           then show ?thesis by simp
         qed
         also have "... = (1 + 8 / 9 / n1 k) ^ (2 ^ k) / 2 powr (4 / 3) ^ (k - 1)"
           unfolding n1_def
           by (smt (verit, best) powr_realpow divide_pos_pos numeral_plus_numeral numeral_plus_one of_nat_numeral of_nat_power semiring_norm(2) zero_less_power)
         also have "... = d k ^ 2 ^ k / 2 powr (4 / 3) ^ (k - 1)"
         proof -
           have **: "8 / 9 / n1 k = (2/3) ^ (k+1)" 
             unfolding n1_def using \<open>k\<ge>1\<close>
             by (simp add: divide_simps split: nat_diff_split)
           then show ?thesis 
             unfolding d_def by presburger 
         qed
         finally show "((1 + 8 / 9 / n1 k) powr n1 k / 2) powr n2 k 
                     = d k ^ 2 ^ k / 2 powr (4 / 3) ^ (k - 1)" .
       qed
       ultimately show ?thesis using filterlim_cong by fast
     qed
     moreover have "\<forall>\<^sub>F n in sequentially. d n ^ 2 ^ n / 2 powr((4/3)^(n-1)) 
         \<le> d n ^ 2 ^ n / real_of_int (b n)"
       using eventually_sequentiallyI[of 6]
       by (smt (verit, best) asscor2 b dgt1 frac_le of_int_0_less_iff zero_le_power)
     ultimately show ?thesis by (auto elim: filterlim_at_top_mono)
   qed
   ultimately show ?thesis using Hancl3[OF \<open>A>1\<close> _ a b _ assu1,of d 6] by force
 qed
 
 end
diff --git a/thys/Transcendence_Series_Hancl_Rucki/Transcendence_Series.thy b/thys/Transcendence_Series_Hancl_Rucki/Transcendence_Series.thy
--- a/thys/Transcendence_Series_Hancl_Rucki/Transcendence_Series.thy
+++ b/thys/Transcendence_Series_Hancl_Rucki/Transcendence_Series.thy
@@ -1,1042 +1,1028 @@
 (* Title:     Transcendence_Series.thy
    Authors:   Angeliki Koutsoukou-Argyraki and Wenda Li, University of Cambridge
 *)
 
 section \<open>The transcendence of certain infinite series\<close>
 theory "Transcendence_Series" imports
     "HOL-Analysis.Multivariate_Analysis"
     "HOL-Computational_Algebra.Polynomial"
     Prime_Number_Theorem.Prime_Number_Theorem_Library
 begin
 
 text \<open>
 We formalise the proofs of two transcendence criteria by J. Han\v{c}l and P. Rucki that
 assert the transcendence of the sums of certain infinite series built up by sequences that 
 fulfil certain properties (Theorems 2.1 and 2.2 in \cite{hancl2005}, HanclRucki1 and HanclRucki2 
 here respectively). Both proofs make use of Roth's celebrated theorem on diophantine approximations 
 to algebraic numbers from 1955 \cite{roth_1955} which we assume and implement within the locale 
 RothsTheorem.
 
-A small mistake was detected in the original proof of Theorem 2.1, and the authors suggested
-to us a fix for the problem (in communication by email). 
+A small mistake was detected in the original proof of Theorem 2.1, and the authors gave us a fix for the problem (by email). 
 Our formalised proof incorporates this correction (see the Remark in the proof of HanclRucki1).
 \<close>
 
 subsection \<open>Misc\<close>
 
 lemma powr_less_inverse_iff:
   fixes x y z::real
-  assumes "x>0""y>0""z>0"
+  assumes "x>0" "y>0" "z>0"
   shows "x powr y < z \<longleftrightarrow> x < z powr (inverse y)"
 proof
   assume "x powr y < z"
   from powr_less_mono2[OF _ _ this,of "inverse y"] 
   show "x < z powr inverse y" 
     using assms by (auto simp:powr_powr)
 next
   assume *:"x < z powr inverse y"
   from powr_less_mono2[OF _ _ *,of y] show "x powr y < z"
     using assms by (auto simp:powr_powr)
 qed
 
 lemma powr_less_inverse_iff':
   fixes x y z::real
-  assumes "x>0""y>0""z>0"
+  assumes "x>0" "y>0" "z>0"
   shows "z< x powr y \<longleftrightarrow> z powr (inverse y) < x"
   using powr_less_inverse_iff[symmetric,of _ "inverse y"] assms by auto
 
 lemma powr_less_eq_inverse_iff:
   fixes x y z::real
-  assumes "x>0""y>0""z>0"
+  assumes "x>0" "y>0" "z>0"
   shows "x powr y \<le> z \<longleftrightarrow> x \<le> z powr (inverse y)"
-  by (meson assms(1) assms(2) assms(3) not_less powr_less_inverse_iff')
+  by (meson assms not_less powr_less_inverse_iff')
 
 lemma powr_less_eq_inverse_iff':
   fixes x y z::real
-  assumes "x>0""y>0""z>0"
-  shows "z\<le> x powr y \<longleftrightarrow> z powr (inverse y) \<le> x"
-  by (simp add: assms(1) assms(2) assms(3) powr_less_eq_inverse_iff)
+  assumes "x>0" "y>0" "z>0"
+  shows "z \<le> x powr y \<longleftrightarrow> z powr (inverse y) \<le> x"
+  by (simp add: assms powr_less_eq_inverse_iff)
 
 lemma tendsto_PInfty_mono:
   assumes "(ereal o f) \<longlonglongrightarrow> \<infinity>" "\<forall>\<^sub>F x in sequentially. f x \<le> g x"
   shows "(ereal o g) \<longlonglongrightarrow> \<infinity>"
   using assms unfolding comp_def tendsto_PInfty_eq_at_top
   by (elim filterlim_at_top_mono, simp)
 
 lemma limsup_infinity_imp_Inf_many:
   assumes "limsup f = \<infinity>"
   shows "(\<forall> m. (\<exists>\<^sub>\<infinity>i. f i > ereal m))" unfolding INFM_nat
 proof (clarify,rule ccontr)
   fix m k assume "\<not> (\<exists>n>k. ereal m < f n)"
   then have "\<forall>n>k. f n \<le> ereal m" by auto
   then have "\<forall>\<^sub>F n in sequentially. f n \<le> ereal m"
     using eventually_at_top_dense by blast
   then have "limsup f \<le> ereal m" using Limsup_bounded by auto
   then show False using assms by simp
 qed
 
 lemma snd_quotient_plus_leq:
   defines "de\<equiv>(snd o quotient_of)"
   shows "de (x+y) \<le> de x * de y "
 proof -                                
   obtain x1 x2 y1 y2 where xy: "quotient_of x = (x1,x2)" "quotient_of y=(y1,y2)"
     by (meson surj_pair)
   have "x2>0" "y2>0" using xy quotient_of_denom_pos by blast+
   then show ?thesis
     unfolding de_def comp_def rat_plus_code xy 
     apply (auto split:prod.split simp:Rat.normalize_def Let_def)
     by (smt div_by_1 gcd_pos_int int_div_less_self mult_eq_0_iff mult_sign_intros(1))
 qed
 
 lemma quotient_of_inj: "inj quotient_of"
   unfolding inj_def by (simp add: quotient_of_inject)
 
 lemma infinite_inj_imageE:
   assumes "infinite A" "inj_on f A" "f ` A \<subseteq> B"
   shows "infinite B"
   using assms inj_on_finite by blast
 
 lemma incseq_tendsto_limsup:
   fixes f::"nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
   assumes "incseq f"
   shows "f \<longlonglongrightarrow> limsup f"
   using LIMSEQ_SUP assms convergent_def convergent_ereal tendsto_Limsup 
           trivial_limit_sequentially by blast
 
 subsection \<open>Main proofs\<close>
 
-text \<open>Since the proof of Roths theorem has not been formalized yet, we implement it into a locale 
-      and used it as an assumption.\<close>
+text \<open>Since the proof of Roth's theorem has not been formalized yet, we formalize the statement in a locale 
+      and use it as an assumption.\<close>
 locale RothsTheorem = 
   assumes RothsTheorem:"\<forall>\<xi> \<kappa>. algebraic \<xi> \<and> \<xi> \<notin> \<rat> \<and> infinite {(p,q). q>0 \<and> 
             coprime p q \<and> \<bar>\<xi> - of_int p / of_int q\<bar> < 1 / q powr \<kappa>} \<longrightarrow> \<kappa> \<le> 2"
 
 theorem (in RothsTheorem) HanclRucki1:
   fixes a b ::"nat\<Rightarrow>int" and \<delta> ::real 
   defines "aa\<equiv>(\<lambda>n. real_of_int (a n))" and "bb\<equiv>(\<lambda>n. real_of_int (b n))"
   assumes a_pos:"\<forall> k. a k >0" and b_pos:"\<forall> k. b k >0" and "\<delta> >0"
       and limsup_infy:"limsup (\<lambda> k. aa (k+1)/(\<Prod>i = 0..k. aa i)powr(2+\<delta>)*(1/bb (k+1))) = \<infinity>" 
       and liminf_1:"liminf (\<lambda>k. aa (k+1) / aa k * bb k / bb (k+1)) > 1"
   shows "\<not> algebraic(suminf  (\<lambda> k. bb k / aa k))" 
 proof -
   have summable:"summable (\<lambda> k. bb k / aa k)" 
   proof (rule ratio_test_convergence)
     have [simp]:"aa k>0" "bb k>0" for k
       unfolding aa_def bb_def using a_pos b_pos by auto
     show "\<forall>\<^sub>F n in sequentially. 0 < bb n / aa n"
-      apply (rule eventuallyI)
       by auto
     show "1 < liminf (\<lambda>n. ereal (bb n / aa n / (bb (Suc n) / aa (Suc n))))" 
       using liminf_1 by (auto simp:algebra_simps) 
   qed
   have [simp]: "aa k>0" "bb k>0" for k unfolding aa_def bb_def 
     by (auto simp add: a_pos b_pos)
   have ab_1:"aa k\<ge>1" "bb k\<ge>1" for k
     unfolding aa_def bb_def using a_pos b_pos 
     by (auto simp add: int_one_le_iff_zero_less)
 
-  define B where "B=liminf (\<lambda>x. ereal (aa (x + 1) / aa x * bb x / bb (x + 1)))"
-  define M where "M= (case B of ereal m \<Rightarrow> (m+1)/2 | _ \<Rightarrow> 2)"
+  define B where "B \<equiv> liminf (\<lambda>x. ereal (aa (x + 1) / aa x * bb x / bb (x + 1)))"
+  define M where "M \<equiv> (case B of ereal m \<Rightarrow> (m+1)/2 | _ \<Rightarrow> 2)"
   have "M > 1" "M < B"
     using liminf_1 unfolding M_def 
-    apply (fold B_def)
-    by (cases B,auto)+
+    by (auto simp add: M_def B_def split: ereal.split)
 
   text \<open>
 Remark:
 In the original proof of Theorem 2.1 in \cite{hancl2005}
 it was claimed in p.534 that from assumption (3) (i.e. @{thm liminf_1}),
 we obtain that:
 $\forall A>1~\exists k_0~ \forall k > k_0~ \frac{1}{A} \frac{b_k}{ a_k} > \frac{ b_{k+1}}{ a_{k+1}} $,
  however note the counterexample  where
 $a_{k+1}= k (a_1 a_2 ... a_k)^{\lceil 2+ \delta \rceil}$ if k is odd, and
 $a_{k+1} = 2 a_k$ otherwise, with $b_k =1$ for all $k$.
 In commmunication by email the authors suggested to replace the claim 
 $\forall A>1~\exists k_0~ \forall k > k_0~ \frac{1}{A} \frac{b_k}{ a_k} > \frac{ b_{k+1}}{ a_{k+1}} $
 with
 $\exists A>1~\exists k_0~ \forall k > k_0~ \frac{1}{A} \frac{b_k}{ a_k} > \frac{ b_{k+1}}{ a_{k+1}} $
 which solves the problem and the proof proceeds as in the paper.
 The witness for $\exists A>1 $ is denoted by $M$ here.\<close>
 
   have bb_aa_event:"\<forall>\<^sub>F k in sequentially. (1/M)*(bb k / aa k)> bb(k+1)/ aa (k+1)"
     using less_LiminfD[OF \<open>M < B\<close>[unfolded B_def],simplified] 
-    apply eventually_elim
-    using \<open>M > 1\<close> by (auto simp:divide_simps algebra_simps)
+    by eventually_elim (use \<open>M > 1\<close> in \<open>auto simp: field_simps\<close>)
 
   have bb_aa_p:"\<forall>\<^sub>F k in sequentially. \<forall>p. bb(k+p)/ aa (k+p) \<le> (1/M^p)*(bb k / aa k)" 
   proof -
     obtain k0 where k0_ineq:
         "\<forall>n\<ge>k0. bb (n + 1) / aa (n + 1) < 1 / M * (bb n / aa n)" 
       using bb_aa_event unfolding eventually_sequentially
       by auto
     have "bb(k+p)/ aa (k+p) \<le> (1/M^p)*(bb k / aa k)" when "k\<ge>k0" for p k
     proof (induct p)
       case 0
       then show ?case by auto
     next
       case (Suc p)
       have " bb (k + Suc p) / aa (k + Suc p)  < 1 / M * (bb (k+p) / aa (k+p))"
         using k0_ineq[rule_format,of "k+p"] that by auto
       also have "... \<le> 1 / M ^(Suc p) * (bb k / aa k)"
         using Suc \<open>M>1\<close> by (auto simp add:field_simps)
       finally show ?case by auto
     qed
     then show ?thesis unfolding eventually_sequentially by auto
   qed
 
   define \<xi> where "\<xi> = suminf (\<lambda> k. bb k / aa k)"
   have \<xi>_Inf_many:"\<exists>\<^sub>\<infinity> k. \<bar>\<xi> - (\<Sum>k = 0..k. bb k / aa k)\<bar> <  1 / prod aa {0..k} powr (2 + \<delta>)" 
   proof -
-    have "\<bar>\<xi> - (\<Sum>i = 0..k. bb i / aa i)\<bar> = \<bar>\<Sum>i. bb (i+(k+1)) / aa (i+(k+1))\<bar>"
-      for k
+    have "\<bar>\<xi> - (\<Sum>i = 0..k. bb i / aa i)\<bar> = \<bar>\<Sum>i. bb (i+(k+1)) / aa (i+(k+1))\<bar>" for k
       unfolding \<xi>_def
       apply (subst suminf_minus_initial_segment[of _ "k+1",OF summable])
       using atLeast0AtMost lessThan_Suc_atMost by auto
-    
+
     moreover have "\<exists>\<^sub>\<infinity> k. \<bar>\<Sum>i. bb(i+(k+1))/ aa (i+(k+1))\<bar>
                             <  1 / prod aa {0..k} powr (2 + \<delta>)" 
     proof -
-      define P where "P = (\<lambda> i. \<forall>p. bb (i + 1 + p) / aa (i + 1 + p)
+      define P where "P \<equiv> (\<lambda> i. \<forall>p. bb (i + 1 + p) / aa (i + 1 + p)
                                           \<le> 1 / M ^ p * (bb (i + 1) / aa (i + 1)))"
-      define Q where "Q= (\<lambda> i. ereal (M / (M - 1)) 
+      define Q where "Q \<equiv> (\<lambda> i. ereal (M / (M - 1)) 
                     < ereal (aa (i + 1) / prod aa {0..i} powr (2 + \<delta>) * (1 / bb (i + 1))))"
       have "\<forall>\<^sub>\<infinity> i. P i"
         using bb_aa_p[THEN sequentially_offset, of 1] cofinite_eq_sequentially
         unfolding P_def by auto
       moreover have "\<exists>\<^sub>\<infinity>i. Q i"
         using limsup_infy[THEN limsup_infinity_imp_Inf_many,rule_format,of "(M / (M -1))"]
         unfolding Q_def .
       moreover have "\<bar>\<Sum>i. bb(i+(k+1))/ aa (i+(k+1))\<bar>
                             <  1 / prod aa {0..k} powr (2 + \<delta>)"
         when "P k" "Q k" for k
       proof -
         have summable_M:"summable (\<lambda>i. 1 / M ^ i)"
           apply (rule summable_ratio_test[of "1/M"])
           using \<open>M>1\<close> by auto
         
         have "(\<Sum>i. bb (i + (k + 1)) / aa (i + (k + 1))) \<ge> 0"
           apply (rule suminf_nonneg)
           subgoal using summable_ignore_initial_segment[OF summable,of "k+1"] by auto 
           subgoal by (simp add: less_imp_le)
           done
         then have "\<bar>\<Sum>i. bb (i + (k + 1)) / aa (i + (k + 1))\<bar> 
                       = (\<Sum>i. bb (i + (k + 1)) / aa (i + (k + 1)))"
           by auto
         also have "... \<le> (\<Sum>i. 1 / M ^ i * (bb (k + 1) / aa (k + 1)))"
           apply (rule suminf_le)
           subgoal using that(1) unfolding P_def by (auto simp add:algebra_simps)
           subgoal using summable_ignore_initial_segment[OF summable,of "k+1"] by auto
           subgoal using summable_mult2[OF summable_M,of " bb (k + 1) / aa (k + 1)"] 
             by auto
           done
         also have "... = (bb (k + 1) / aa (k + 1)) * (\<Sum>i. 1 / M ^ i)"
           using suminf_mult2[OF summable_M,of " bb (k + 1) / aa (k + 1)"]
           by (auto simp:algebra_simps)
         also have "... = (bb (k + 1) / aa (k + 1)) * (\<Sum>i. (1 / M) ^ i)"
           using \<open>M>1\<close> by (auto simp: field_simps)
         also have "... = (bb (k + 1) / aa (k + 1)) * (M / (M -1))"
           apply (subst suminf_geometric) 
           using \<open>M>1\<close>  by (auto simp: field_simps)
         also have "... < (bb (k + 1) / aa (k + 1)) * (aa (k + 1) / 
                             prod aa {0..k} powr (2 + \<delta>) * (1 / bb (k + 1)))"
           apply (subst mult_less_cancel_left_pos)
           using that(2) unfolding Q_def by auto
         also have "... = 1/ prod aa {0..k} powr (2 + \<delta>)"
           using ab_1[of "Suc k"] by auto
         finally show ?thesis .
       qed
       ultimately show ?thesis by (smt INFM_conjI INFM_mono)
     qed
     ultimately show ?thesis by auto
   qed
 
-  define pq where "pq = (\<lambda>k. quotient_of (\<Sum>i=0..k. of_int (b i) / of_int (a i)))"
-  define p q where "p = fst \<circ> pq" and "q = snd \<circ> pq"
+  define pq where "pq \<equiv> (\<lambda>k. quotient_of (\<Sum>i=0..k. of_int (b i) / of_int (a i)))"
+  define p q where "p \<equiv> fst \<circ> pq" and "q = snd \<circ> pq"
   have coprime_pq:"coprime (p k) (q k)"
         and q_pos:"q k > 0" and pq_sum:"p k / q k = (\<Sum>i=0..k. b i / a i)" for k
   proof -
     have eq: "quotient_of (\<Sum>i=0..k. of_int (b i) / of_int (a i)) = (p k, q k)"
       by (simp add: p_def q_def pq_def)
     from quotient_of_coprime[OF eq] show "coprime (p k) (q k)" .
     from quotient_of_denom_pos[OF eq] show "q k > 0" .
     have "(\<Sum>i=0..k. b i / a i) = of_rat (\<Sum>i=0..k. of_int (b i) / of_int (a i))"
       by (simp add: of_rat_sum of_rat_divide)
     also have "(\<Sum>i=0..k. rat_of_int (b i) / rat_of_int (a i)) =
                  rat_of_int (p k) / rat_of_int (q k)"
       using quotient_of_div[OF eq] by simp
     finally show "p k / q k = (\<Sum>i=0..k. b i / a i)" by (simp add:of_rat_divide)
   qed
 
-  have \<xi>_Inf_many2:"\<exists>\<^sub>\<infinity> k. \<bar>\<xi> - p k / q k\<bar> 
-                        <  1 / q k powr (2 + \<delta>)"
+  have \<xi>_Inf_many2:"\<exists>\<^sub>\<infinity> k. \<bar>\<xi> - p k / q k\<bar> <  1 / q k powr (2 + \<delta>)"
     using \<xi>_Inf_many
   proof (elim INFM_mono)
     fix k assume asm:"\<bar>\<xi> - (\<Sum>k = 0..k. bb k / aa k)\<bar> < 1 / prod aa {0..k} powr (2 + \<delta>)"
     have "\<bar>\<xi> - real_of_int (p k) / real_of_int (q k)\<bar> 
               = \<bar>\<xi> - (\<Sum>k = 0..k. bb k / aa k)\<bar>"
       using pq_sum unfolding aa_def bb_def by auto
     also have "... < 1 / prod aa {0..k} powr (2 + \<delta>)"
       using asm by auto
     also have "... \<le> 1 / q k powr (2 + \<delta>)"
     proof -
       have "q k \<le> prod aa {0..k}"
       proof (induct k)
         case 0
         then show ?case unfolding q_def pq_def aa_def 
           apply (simp add:rat_divide_code of_int_rat quotient_of_Fract)
           using ab_1[of 0,unfolded aa_def bb_def] unfolding Let_def normalize_def 
           apply auto
           by (metis div_by_1 gcd_pos_int less_imp_le less_trans nonneg1_imp_zdiv_pos_iff 
                 not_less zdiv_mono2)  
       next
         case (Suc k)
-        define de where "de=snd \<circ> quotient_of"
+        define de where "de \<equiv>snd \<circ> quotient_of"
         have "real_of_int (q (Suc k)) 
                   = de (\<Sum>i=0..Suc k. of_int (b i) / of_int (a i))"
           unfolding q_def pq_def de_def by simp
         also have "... = de ((\<Sum>i=0..k. of_int (b i) / of_int (a i)) 
                                 + of_int (b (Suc k)) / of_int (a (Suc k)))"
           by simp
         also have "... \<le> de (\<Sum>i=0..k. of_int (b i) / of_int (a i)) 
                                 * de (of_int (b (Suc k)) / of_int (a (Suc k)))"          
           using snd_quotient_plus_leq[folded de_def] by presburger
         also have "... = q k * de (of_int (b (Suc k)) / of_int (a (Suc k)))"
           unfolding q_def pq_def de_def by auto
         also have "... = q k * snd (Rat.normalize (b (Suc k), a (Suc k)))"
           by (simp add:rat_divide_code of_int_rat quotient_of_Fract de_def)
         also have "... \<le> q k * aa (Suc k)"
           using ab_1[of "Suc k"] q_pos[of "k"] 
           unfolding normalize_def aa_def bb_def Let_def
           apply auto
           by (metis div_by_1 int_one_le_iff_zero_less less_trans 
                   nonneg1_imp_zdiv_pos_iff not_less zdiv_mono2 zero_less_one)
         also have "... \<le>  prod aa {0..k} * aa (Suc k)"
           using Suc ab_1[of "Suc k"] by auto
         also have "... = prod aa {0..Suc k}"
           by (simp add: prod.atLeast0_atMost_Suc)
         finally show ?case .
       qed 
       then show ?thesis 
         by (smt \<open>0 < \<delta>\<close> frac_le of_int_0 of_int_le_iff powr_gt_zero 
                   powr_mono2 q_pos)
     qed
     finally show "\<bar>\<xi> - real_of_int (p k) / real_of_int (q k)\<bar> < 1 / real_of_int (q k) powr (2 + \<delta>)" .
   qed
 
-  define pqs where "pqs={(p, q). q>0 \<and> coprime p q 
+  define pqs where "pqs \<equiv>{(p, q). q>0 \<and> coprime p q 
       \<and> \<bar>\<xi> - real_of_int p / real_of_int q\<bar> < 1 / q powr (2 + \<delta>)}"
   have \<xi>_infinite:"infinite pqs"
   proof -
-    define A where "A={k. \<bar>\<xi> -  (p k) /  (q k)\<bar> < 1 / (q k) powr (2 + \<delta>)}" 
+    define A where "A \<equiv> {k. \<bar>\<xi> -  (p k) /  (q k)\<bar> < 1 / (q k) powr (2 + \<delta>)}" 
     have "\<exists>\<^sub>\<infinity> k. \<bar>\<xi> - p k / q k\<bar> <  1 / q k powr (2 + \<delta>)"
       using \<xi>_Inf_many2 .
     then have "infinite A"
       unfolding Inf_many_def A_def by auto
     moreover have "inj_on (\<lambda>k. (p k, q k)) A"
     proof -
-      define g where "g=(\<lambda>i. rat_of_int (b i) / rat_of_int (a i))"
-      define f where "f=(\<lambda>k. \<Sum>i = 0..k. g i)"
+      define g where "g \<equiv> (\<lambda>i. rat_of_int (b i) / rat_of_int (a i))"
+      define f where "f \<equiv> (\<lambda>k. \<Sum>i = 0..k. g i)"
       have g_pos:"g i>0" for i
         unfolding g_def by (simp add: a_pos b_pos)
       have "strict_mono f" unfolding strict_mono_def f_def
       proof safe
         fix x y::nat assume "x < y"
         then have "sum g {0..y} - sum g {0..x} = sum g {x<..y}" 
           apply (subst  Groups_Big.sum_diff[symmetric])
           by (auto intro:arg_cong2[where f=sum])
         also have "... > 0"
           apply (rule ordered_comm_monoid_add_class.sum_pos)
           using \<open>x<y\<close> g_pos by auto
         finally have "sum g {0..y} - sum g {0..x} >0" .
         then show "sum g {0..x} < sum g {0..y}" by auto
       qed
       then have "inj f" using strict_mono_imp_inj_on by auto
       then have "inj (quotient_of o f)" by (simp add: inj_compose quotient_of_inj)
       then have "inj (\<lambda>k. (p k, q k))"
         unfolding f_def p_def q_def pq_def comp_def
         apply (fold g_def)
         by auto
       then show ?thesis by (auto elim:subset_inj_on)
     qed
     moreover have "(\<lambda>k. (p k, q k)) ` A \<subseteq> pqs"
       unfolding A_def pqs_def using coprime_pq q_pos by auto
     ultimately show ?thesis
       apply (elim infinite_inj_imageE)
       by auto
   qed
   moreover have "finite pqs" if "\<xi> \<in> \<rat>"
   proof -
     obtain m n where \<xi>_mn:"\<xi> = (of_int m / of_int n)" and "coprime m n" "n>0"
     proof -
       obtain m n where mn:"\<bar>\<xi>\<bar> = (of_nat m / of_nat n)" "coprime m n" "n\<noteq>0"
         using Rats_abs_nat_div_natE[OF \<open>\<xi> \<in> \<rat>\<close> Rats_abs_nat_div_natE]
         by metis
       define m' and n'::int 
         where "m'=(if \<xi> > 0 then nat m else -nat m)" and "n'=nat n"
       then have "\<xi> = (of_int m' / of_int n')" "coprime m' n'" "n'>0"
         using mn by auto
       then show ?thesis using that by auto
     qed
     have "pqs \<subseteq> {(m,n)} \<union> {x. x \<in>pqs \<and> - \<bar>m\<bar> - 1 \<le>fst x \<and> fst x \<le> \<bar>m\<bar> + 1 \<and> 0<snd x \<and> snd x < n }"
     proof (rule subsetI)
       fix x assume "x \<in> pqs"
-      define p q where "p=fst x" and "q=snd x"
+      define p q where "p \<equiv> fst x" and "q=snd x"
       have "q>0" "coprime p q" and pq_less:"\<bar>\<xi> - p / q\<bar> < 1 / q powr (2 + \<delta>)"
         using \<open>x\<in>pqs\<close> unfolding p_def q_def pqs_def by auto
       have q_lt_n:"q<n" when "m\<noteq>p \<or> n\<noteq>q" 
       proof -
         have "m * q \<noteq> n * p" using that \<open>coprime m n\<close> \<open>coprime p q\<close> \<open>q>0\<close> \<open>n>0\<close> 
           by (metis eq_rat(1) fst_conv int_one_le_iff_zero_less mult.commute normalize_stable 
                 not_one_le_zero quotient_of_Fract snd_conv)
         then have "1/(n*q) \<le> \<bar>m/n - p/q\<bar>"
           using \<open>q>0\<close> \<open>n>0\<close>  
           apply (auto simp:field_simps)
           by (metis add_diff_cancel_left' diff_diff_eq2 diff_zero less_irrefl not_le of_int_diff 
                 of_int_lessD of_int_mult)
         also have "...  < 1 / q powr (2 + \<delta>)"
           using pq_less unfolding \<xi>_mn by auto
         also have "... \<le> 1 / q ^2"
         proof -
           have "real_of_int (q\<^sup>2) = q powr 2"
             apply (subst powr_numeral)
             unfolding power2_eq_square using \<open>q>0\<close> by auto
           also have "... \<le> q powr (2 + \<delta>)"
             apply (rule powr_mono)
             using \<open>q>0\<close> \<open>\<delta>>0\<close> by auto
           finally have "real_of_int (q\<^sup>2) \<le> real_of_int q powr (2 + \<delta>)" .
           moreover have "real_of_int q powr (2 + \<delta>) > 0" using \<open>0 < q\<close> by auto
           ultimately show ?thesis by (auto simp:field_simps)
         qed 
         finally have " 1 /  (n * q) < 1 / q\<^sup>2" .
         then show ?thesis  using \<open>q>0\<close> \<open>n>0\<close> 
           unfolding power2_eq_square by (auto simp:field_simps)
       qed
       moreover have "- \<bar>m\<bar> - 1 \<le> p \<and> p \<le> \<bar>m\<bar> + 1" when "m\<noteq>p \<or> n\<noteq>q" 
       proof -
-        define qn where "qn=q/n"
+        define qn where "qn \<equiv> q/n"
         have "0<qn" "qn<1" unfolding qn_def using q_lt_n[OF \<open>m\<noteq>p \<or> n\<noteq>q\<close>] \<open>q>0\<close> by auto
 
         have "\<bar>m/n - p / q\<bar> < 1 / q powr (2 + \<delta>)" using pq_less unfolding \<xi>_mn by simp
         then have "\<bar>p / q - m/n\<bar> < 1 / q powr (2 + \<delta>)" by simp
         then have " m/n- 1 / q powr (2 + \<delta>) < p/q \<and> p/q < m/n + 1 / q powr (2 + \<delta>)"
           unfolding abs_diff_less_iff by auto
         then have "qn*m- q / q powr (2 + \<delta>) < p \<and> p < qn*m + q / q powr (2 + \<delta>)"
           unfolding qn_def using \<open>q>0\<close> by (auto simp:field_simps)
         moreover have "- \<bar>m\<bar> - 1 \<le> qn*m- q / q powr (2 + \<delta>)"
         proof -
           have "- \<bar>m\<bar> \<le> qn*m" using \<open>0<qn\<close> \<open>qn<1\<close> 
             apply (cases "m\<ge>0")
             subgoal 
               apply simp 
               by (meson less_eq_real_def mult_nonneg_nonneg neg_le_0_iff_le of_int_0_le_iff order_trans)
             subgoal by simp
             done
           moreover have "- 1 \<le> - q / q powr (2 + \<delta>)" 
           proof -
             have "q = q powr 1" using \<open>0 < q\<close> by auto
             also have "... \<le>q powr (2 + \<delta>)"
               apply (rule powr_mono)
               using \<open>q>0\<close> \<open>\<delta>>0\<close> by auto
             finally have "q \<le> q powr (2 + \<delta>)" .
             then show ?thesis using \<open>0 < q\<close> by auto
           qed
           ultimately show ?thesis by auto
         qed
         moreover have "qn*m + q / q powr (2 + \<delta>) \<le> \<bar>m\<bar> + 1"
         proof -
           have "qn*m \<le> \<bar>m\<bar>" using \<open>0<qn\<close> \<open>qn<1\<close> 
             apply (cases "m\<ge>0")
             subgoal by (simp add: mult_left_le_one_le)
             subgoal by (smt of_int_0_le_iff zero_le_mult_iff)
             done
           moreover have "q / q powr (2 + \<delta>) \<le> 1"
           proof -
             have "q = q powr 1" using \<open>0 < q\<close> by auto
             also have "... \<le>q powr (2 + \<delta>)"
               apply (rule powr_mono)
               using \<open>q>0\<close> \<open>\<delta>>0\<close> by auto
             finally have "q \<le> q powr (2 + \<delta>)" .
             then show ?thesis using \<open>0 < q\<close> by auto
           qed
           ultimately show ?thesis by auto
         qed
         ultimately show ?thesis by auto
       qed
       ultimately show "x \<in> {(m, n)} \<union> {x \<in> pqs. - \<bar>m\<bar> - 1 \<le> fst x \<and> fst x \<le> \<bar>m\<bar> + 1 
                           \<and> 0 < snd x \<and> snd x < n}" 
         using \<open>x \<in> pqs\<close> \<open>q>0\<close> unfolding p_def q_def by force
     qed
     moreover have "finite {x. x \<in>pqs \<and> - \<bar>m\<bar> - 1 \<le>fst x \<and> fst x \<le> \<bar>m\<bar> + 1 \<and> 0<snd x \<and> snd x < n }" 
     proof -
       have "finite ({- \<bar>m\<bar> - 1..\<bar>m\<bar> +1} \<times> {0<..<n})" by blast
       moreover have "{x. x \<in>pqs \<and> - \<bar>m\<bar> - 1 \<le>fst x \<and> fst x \<le> \<bar>m\<bar> + 1 \<and> 0<snd x \<and> snd x < n } \<subseteq> 
                 ({- \<bar>m\<bar> - 1..\<bar>m\<bar> +1} \<times> {0<..<n})"
         by auto
       ultimately show ?thesis 
         apply (elim rev_finite_subset)
         by blast
     qed
     ultimately show ?thesis using finite_subset by auto
   qed
   ultimately show ?thesis 
     apply (fold \<xi>_def)
     using RothsTheorem[rule_format,of \<xi> "2 + \<delta>",folded pqs_def] \<open>\<delta> >0\<close> by auto
 qed
 
 
 theorem (in RothsTheorem) HanclRucki2: 
   fixes a b ::"nat\<Rightarrow>int" and \<delta> \<epsilon> ::real 
   defines "aa\<equiv>(\<lambda>n. real_of_int (a n))" and "bb\<equiv>(\<lambda>n. real_of_int (b n))"
   assumes a_pos:"\<forall> k. a k >0" and b_pos:"\<forall> k. b k >0" and "\<delta> >0"
     and "\<epsilon> >0" 
     and limsup_infi:"limsup (\<lambda> k.(aa (k+1)/(\<Prod>i = 0..k. aa i)powr(2+(2/\<epsilon>) + \<delta>))
           * (1/(bb (k+1)))) = \<infinity>"
     and ratio_large:"\<forall> k. ( k \<ge> t \<longrightarrow>  (( aa(k+1)/bb( k+1)) ) powr(1/(1+\<epsilon>)) 
               \<ge>  (( aa k/bb k) powr(1/(1+\<epsilon>)))+1)"
   shows "\<not> algebraic(suminf (\<lambda> k. bb k /aa k))  "
 proof-
   have aa_bb_pos[simp]:"aa k>0" "bb k>0" for k
     unfolding aa_def bb_def using a_pos b_pos by auto
   have summable:"summable (\<lambda> k. bb k / aa k)"
   proof -
     define c0 where "c0\<equiv>(aa t/bb t) powr(1/(1+\<epsilon>)) - t"
     have ab_k:"(aa k / bb k) powr(1/(1+\<epsilon>)) \<ge> k + c0" when "k\<ge>t" for k
       using that
     proof (induct k)
       case 0
       then show ?case unfolding c0_def by simp
     next
       case (Suc k)
       have ?case when "\<not> t\<le>k"
       proof -
         have "t = Suc k" using that Suc.prems by linarith
         then show ?thesis unfolding c0_def by auto
       qed
       moreover have ?case when "t \<le> k"
       proof -
         have "(aa(k+1)/bb(k+1)) powr(1/(1+\<epsilon>))
               \<ge> ( aa k/bb k) powr(1/(1+\<epsilon>))+1" 
           using ratio_large[rule_format,OF that] by blast
         then show ?thesis using Suc(1)[OF that] by simp
       qed
       ultimately show ?case by auto
     qed
     have "summable (\<lambda>k. 1 / (k + c0) powr (1+\<epsilon>))"
     proof -
       have "c0 + t > 0" unfolding c0_def
         using aa_bb_pos[of t] by (simp,linarith)
       then have "summable (\<lambda>k. 1 / (k + (c0+t)) powr (1+\<epsilon>))"
         using summable_hurwitz_zeta_real[of "1+\<epsilon>" "c0+t"]
         apply (subst (asm) powr_minus_divide)
         using \<open>\<epsilon>>0\<close> by auto
       then show ?thesis
         apply (rule_tac summable_offset[of _ t])
         by (auto simp:algebra_simps)
     qed
     moreover have "bb k / aa k \<le> 1 / (k + c0) powr (1+\<epsilon>)" when "k\<ge>t" for k
     proof -
       have "(aa t / bb t) powr (1 / (1 + \<epsilon>)) > 0"
         apply simp
         by (metis \<open>\<And>k. 0 < aa k\<close> \<open>\<And>k. 0 < bb k\<close> less_numeral_extra(3))
       then have "k + c0 >0" unfolding c0_def using that by linarith 
       then have "aa k / bb k \<ge> (k + c0) powr (1+\<epsilon>)" 
         using ab_k[OF that] 
         apply (subst (asm) powr_less_eq_inverse_iff')
         using \<open>\<epsilon> >0\<close> by auto
       then have "inverse (aa k / bb k) \<le> inverse ((k + c0) powr (1+\<epsilon>))" 
         apply (elim le_imp_inverse_le)
         using \<open>k + c0 >0\<close> by auto
       then show ?thesis by (simp add: inverse_eq_divide)
     qed
     ultimately show ?thesis 
       apply (elim summable_comparison_test'[where N=t])
       using aa_bb_pos by (simp add: less_eq_real_def)
   qed
 
   have 7:"\<exists>\<^sub>\<infinity> k. 1 / (M powr (\<epsilon>/(1+\<epsilon>)) * (\<Prod>i = 0..k. aa i)
                   powr(2+ \<delta> * \<epsilon> / (1+\<epsilon>))) > (bb (k+1) / aa(k+1)) powr (\<epsilon> / (1+\<epsilon>))"
       when "M > 0" for M
   proof -
-    define tt where "tt= (\<lambda>i. prod aa {0..i} powr (2 + 2 / \<epsilon> + \<delta>))"
+    define tt where "tt \<equiv> (\<lambda>i. prod aa {0..i} powr (2 + 2 / \<epsilon> + \<delta>))"
     have tt_pos:"tt i > 0" for i 
       unfolding tt_def
       apply(subst powr_gt_zero,induct i)
       subgoal by (metis aa_bb_pos(1) order_less_irrefl prod_pos)
       subgoal by (metis \<open>\<And>k. 0 < aa k\<close> order_less_irrefl prod_pos)
       done
     have "\<exists>\<^sub>\<infinity>i. M < (aa (i + 1) / tt i * (1 / bb (i + 1)))"
       using limsup_infinity_imp_Inf_many[OF limsup_infi,rule_format,of M]
       unfolding tt_def by auto
     then have "\<exists>\<^sub>\<infinity>i. 1 / (M * tt i) > (bb (i+1) / aa (i+1))"
       apply (elim INFM_mono)
       using \<open>M>0\<close> tt_pos by (auto simp:divide_simps algebra_simps)
     then have "\<exists>\<^sub>\<infinity>i. (1 / (M * tt i)) powr (\<epsilon>/(1+\<epsilon>)) 
                         > (bb (i+1) / aa (i+1)) powr (\<epsilon>/(1+\<epsilon>))"
       apply (elim INFM_mono powr_less_mono2[rotated 2])
       by (simp_all add: assms(6) pos_add_strict less_eq_real_def)
     moreover have "tt i  powr (\<epsilon>/(1+\<epsilon>)) = prod aa {0..i} powr (2 + \<delta> * \<epsilon> / (1+\<epsilon>))"
         for i
       unfolding tt_def
       apply (auto simp:powr_powr)
       using \<open>\<epsilon>>0\<close> by (simp add:divide_simps,simp add:algebra_simps)
     ultimately show ?thesis 
       apply (elim INFM_mono)
       by (smt nonzero_mult_div_cancel_left powr_divide powr_mult powr_one_eq_one
                 that tt_pos zero_less_divide_iff)
   qed
 
   have 8:"\<forall>\<^sub>F k in sequentially. \<forall>s.  (( aa(k+s)/bb( k+s))) \<ge> 
                     ((( aa k/bb k) powr(1/(1+\<epsilon>))) +s)powr(1+\<epsilon>)" 
     using eventually_ge_at_top[of t]
   proof eventually_elim
     case (elim k)
-    define ff where "ff=(\<lambda>k. (aa k / bb k) powr (1 / (1 + \<epsilon>)))"
+    define ff where "ff \<equiv> (\<lambda>k. (aa k / bb k) powr (1 / (1 + \<epsilon>)))"
     have 11:"ff k+s \<le> ff (k+s)" for s
     proof (induct s)
       case 0
       then show ?case unfolding ff_def by auto
     next
       case (Suc s)
       then have "ff k + Suc s \<le> ff (k+Suc s)"
         using ratio_large[rule_format,of "k+s"] \<open> t \<le> k\<close> unfolding ff_def by auto
       then show ?case by simp
     qed
     then have "(ff k+s) powr (1+\<epsilon>) \<le> ff (k+s) powr (1+\<epsilon>)" for s
       apply (rule powr_mono2[of "1+\<epsilon>",rotated 2])
       unfolding ff_def using \<open>\<epsilon>>0\<close> by auto
     then show ?case unfolding ff_def using \<open>\<epsilon>>0\<close> 
       apply (auto simp add:powr_powr)
       by (simp add: a_pos aa_def b_pos bb_def le_less)
   qed
 
   have 9: "(\<Sum>r. 1/((z+real r)powr(1+\<epsilon>))) \<le> 1/(\<epsilon> *(z-1) powr \<epsilon>)" 
       "summable (\<lambda>i. 1/((z+ real i)powr(1+\<epsilon>)))"
     when "z>1" for z
   proof -
-    define f where "f= (\<lambda>r. 1/((z+ r)powr(1+\<epsilon>)))"
+    define f where "f \<equiv> (\<lambda>r. 1/((z+ r)powr(1+\<epsilon>)))"
     have "((\<lambda>x. f (x - 1)) has_integral ((z-1) powr - \<epsilon>) / \<epsilon>) {0..}"
     proof -
        have "((\<lambda>x. (z-1 + x) powr (- 1 - \<epsilon>)) has_integral ((z-1) powr - \<epsilon>) / \<epsilon>) {0<..}"
         using powr_has_integral_at_top[of 0 "z-1" "- 1 - \<epsilon>",simplified] \<open>z>1\<close> \<open>\<epsilon>>0\<close>
         by auto
       then have "((\<lambda>x. (z-1 + x) powr (- 1 - \<epsilon>)) has_integral ((z-1) powr - \<epsilon>) / \<epsilon>) {0..}"
         apply (subst (asm) has_integral_closure[symmetric])
         by (auto simp add: negligible_convex_frontier)
       then show ?thesis 
         apply (rule has_integral_cong[THEN iffD1, rotated 1])
         unfolding f_def by (smt powr_minus_divide)
     qed
     moreover have "\<And>x. 0 \<le> x \<Longrightarrow> 0 \<le> f (x - 1)" unfolding f_def by simp
     moreover have "\<And>x y. 0 \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> f (y - 1) \<le> f (x - 1)" unfolding f_def 
       by (smt assms(6) frac_le powr_mono2 powr_nonneg_iff that)
     ultimately have "summable (\<lambda>i. f (real i))" "(\<Sum>i. f (real i)) \<le> (z - 1) powr - \<epsilon> / \<epsilon>"
       using decreasing_sum_le_integral[of "\<lambda>x. f (x-1)" "((z-1) powr - \<epsilon>) / \<epsilon>",simplified]
       by auto
     moreover have "(z - 1) powr - \<epsilon> / \<epsilon> = 1/(\<epsilon> *(z-1) powr \<epsilon>)"
       by (simp add: powr_minus_divide)
     ultimately show "(\<Sum>i. f (real i)) \<le> 1/(\<epsilon> *(z-1) powr \<epsilon>)" by auto
     show "summable (\<lambda>i. f (real i))" using \<open>summable (\<lambda>i. f (real i))\<close> .
   qed
 
   have u:"(\<lambda>k.( aa k / bb k)) \<longlonglongrightarrow> \<infinity>" 
   proof -
     define ff where "ff\<equiv>(\<lambda>x. ereal (aa x / bb x))"
     have "limsup ff =  \<infinity>" 
     proof -
-      define tt where "tt= (\<lambda>i. prod aa {0..i} powr (2 + 2 / \<epsilon> + \<delta>))"
+      define tt where "tt \<equiv> (\<lambda>i. prod aa {0..i} powr (2 + 2 / \<epsilon> + \<delta>))"
       have "tt i \<ge> 1" for i
         unfolding tt_def
         apply (rule ge_one_powr_ge_zero)
         subgoal 
           apply (rule linordered_nonzero_semiring_class.prod_ge_1)
           by (simp add: a_pos aa_def int_one_le_iff_zero_less)
         subgoal by (simp add: \<open>\<epsilon>>0\<close> \<open>\<delta>>0\<close> less_imp_le)
         done
       then have "limsup (\<lambda>x.  (aa (x + 1) / tt x * (1 / bb (x + 1))))
                   \<le> limsup (\<lambda>x.  aa (x + 1) / bb (x + 1))"
         apply (intro Limsup_mono eventuallyI)
         apply (auto simp add:field_simps order.order_iff_strict)
         by (metis aa_bb_pos(1) div_by_1 frac_less2 less_irrefl less_numeral_extra(1) 
             not_le)
       also have "... = limsup (\<lambda>x.  aa x / bb x)"
         by (subst limsup_shift,simp)
       finally have "limsup (\<lambda>x. ereal (aa (x + 1) / tt x * (1 / bb (x + 1))))
                       \<le> limsup (\<lambda>x. ereal (aa x / bb x))" .
       moreover have "limsup (\<lambda>x. ereal (aa (x + 1) / tt x * (1 / bb (x + 1))))
                         = \<infinity>" using limsup_infi unfolding tt_def by auto
       ultimately show ?thesis 
         unfolding ff_def using ereal_infty_less_eq2(1) by blast
     qed
     then have "limsup (\<lambda>k. ff (k+t)) =  \<infinity>" 
       by (simp add: limsup_shift_k)
     moreover have "incseq (\<lambda>k. ff (k+t))"
     proof (rule incseq_SucI)
       fix k::nat 
       define gg where "gg\<equiv>(\<lambda>x. (aa x / bb x))"
       have "(gg (k+t)) powr (1 / (1 + \<epsilon>)) + 1 
                 \<le> (gg (Suc (k+t))) powr (1 / (1 + \<epsilon>))"
         using ratio_large[rule_format, of "k+t",simplified] unfolding gg_def
         by auto
       then have "(gg (k+t)) powr (1 / (1 + \<epsilon>))
                       \<le> (gg (Suc (k+t))) powr (1 / (1 + \<epsilon>))"
         by auto
       then have "gg (k+t)\<le> gg (Suc (k+t))"
         by (smt aa_bb_pos(1) aa_bb_pos(2) assms(6) divide_pos_pos gg_def 
                 powr_less_mono2)
       then show "ff (k + t) \<le> ff (Suc k + t)" 
         unfolding gg_def ff_def by auto
     qed
     ultimately have "(\<lambda>k. ff (k+t)) \<longlonglongrightarrow> \<infinity>" using incseq_tendsto_limsup
       by fastforce
     then show ?thesis unfolding ff_def 
       unfolding tendsto_def
       apply (subst eventually_sequentially_seg[symmetric,of _ t])
       by simp
   qed
 
   define \<xi> where "\<xi> = suminf (\<lambda> k. bb k / aa k)"
   have 10:"\<forall>\<^sub>F k in sequentially. \<bar>\<xi> - (\<Sum>k = 0..k. bb k / aa k)\<bar> 
                         < 2 / \<epsilon> * (bb (k+1) / aa (k+1)) powr (\<epsilon> / (1+\<epsilon>))" 
     using 8[THEN sequentially_offset,of 1] eventually_ge_at_top[of t]
             u[unfolded tendsto_PInfty,rule_format,THEN sequentially_offset
                         ,of "(2 powr (1/\<epsilon>) / (2 powr (1/\<epsilon>) - 1)) powr (1+\<epsilon>)" 1]
   proof eventually_elim
     case (elim k)
-    define tt where "tt=(aa (k + 1) / bb (k + 1)) powr (1 / (1 + \<epsilon>))"
+    define tt where "tt \<equiv> (aa (k + 1) / bb (k + 1)) powr (1 / (1 + \<epsilon>))"
     have "tt>1"
     proof -
       have "(aa k / bb k) powr (1 / (1 + \<epsilon>)) > 0"
         by (metis a_pos aa_def b_pos bb_def divide_eq_0_iff less_irrefl 
                 of_int_eq_0_iff powr_gt_zero)
       then show ?thesis using ratio_large[rule_format,OF \<open>k\<ge>t\<close>] unfolding tt_def by argo
     qed
     have "\<bar>\<xi> - (\<Sum>i = 0..k. bb i / aa i)\<bar> = \<bar>\<Sum>i. bb (i+(k+1)) / aa (i+(k+1))\<bar>"
       unfolding \<xi>_def
       apply (subst suminf_minus_initial_segment[of _ "k+1",OF summable])
       using atLeast0AtMost lessThan_Suc_atMost by auto
     also have "... = (\<Sum>i. bb (i+(k+1)) / aa (i+(k+1)))"
     proof -
       have "(\<Sum>i. bb (i+(k+1)) / aa (i+(k+1))) > 0"
         apply (rule suminf_pos)
         subgoal using summable[THEN summable_ignore_initial_segment,of "k+1"] .
         subgoal by (simp add: a_pos aa_def b_pos bb_def)
         done
       then show ?thesis by auto
     qed
     also have "... \<le> (\<Sum>i. 1 / (tt + i) powr (1 + \<epsilon>))"
     proof (rule suminf_le)
-      define ff where "ff=(\<lambda>k n. (aa (k+1) / bb (k+1)) powr (1 / (1 + \<epsilon>)) + real n)"
+      define ff where "ff \<equiv> (\<lambda>k n. (aa (k+1) / bb (k+1)) powr (1 / (1 + \<epsilon>)) + real n)"
       have "bb (n + (k + 1)) / aa (n + (k + 1)) \<le> 1 / (ff k n) powr (1 + \<epsilon>)" for n
       proof -
         have "ff k n powr (1 + \<epsilon>) \<le> aa (k + n +1 ) / bb (k + n+1 )"
           using elim(1)[rule_format,of n] unfolding ff_def by auto
         moreover have "ff k n powr (1 + \<epsilon>) > 0" 
           unfolding ff_def by (smt elim(2) of_nat_0_le_iff powr_gt_zero ratio_large)
         ultimately have "1 / ff k n powr (1 + \<epsilon>) \<ge>  bb (k + (n + 1)) / aa (k + (n + 1))"
           apply (drule_tac le_imp_inverse_le)
           by (auto simp add: inverse_eq_divide)
         then show ?thesis by (auto simp:algebra_simps)
       qed
       then show "\<And>n. bb (n + (k + 1)) / aa (n + (k + 1)) \<le> 1 / (tt + real n) powr (1 + \<epsilon>)"
         unfolding ff_def tt_def by auto
       show "summable (\<lambda>i. bb (i + (k + 1)) / aa (i + (k + 1)))" 
         using summable[THEN summable_ignore_initial_segment,of "k+1"] .
       show "summable (\<lambda>x. 1 / (tt + real x) powr (1 + \<epsilon>))" 
         using 9(2)[OF \<open>tt>1\<close>] .
     qed
     also have "... \<le> 1/(\<epsilon> *(tt-1) powr \<epsilon>)" 
       using 9[OF \<open>tt>1\<close>] by simp
     also have "... < 2 / (\<epsilon> *tt powr \<epsilon>)"
     proof -
       have "((2 powr (1/\<epsilon>) / (2 powr (1/\<epsilon>) - 1)) powr (1 + \<epsilon>)) < (aa (k+1) / bb (k+1))"
         using elim(3) by auto
       then have "2 powr (1/\<epsilon>) / (2 powr (1/\<epsilon>) - 1) < tt"
         unfolding tt_def 
         apply (drule_tac powr_less_mono2[rotated 2,where a="1/ (1 + \<epsilon>)"])
         using \<open>\<epsilon>>0\<close> apply (auto simp:powr_powr )
         by (subst (asm) powr_one,auto simp add:field_simps)
       then have " tt < (tt-1) * (2 powr (1/\<epsilon>))"
         using \<open>\<epsilon>>0\<close> by (auto simp:divide_simps algebra_simps) 
       then have "tt powr \<epsilon> < 2 * (tt - 1) powr \<epsilon>"
         apply (drule_tac powr_less_mono2[rotated 2,where a="\<epsilon>"])
         using \<open>\<epsilon>>0\<close> \<open>tt>1\<close> by (auto simp:powr_powr powr_mult)
       then show ?thesis 
         using \<open>\<epsilon>>0\<close> \<open>tt>1\<close> by (auto simp:divide_simps)
     qed
     also have "... =  2 / \<epsilon> * (bb (k + 1) / aa (k + 1)) powr (\<epsilon> / (1 + \<epsilon>))"
       unfolding tt_def 
       using \<open>\<epsilon>>0\<close> 
       by (auto simp:powr_powr divide_simps algebra_simps powr_divide less_imp_le)
     finally show ?case .
   qed
 
-  define pq where "pq = (\<lambda>k. quotient_of (\<Sum>i=0..k. of_int (b i) / of_int (a i)))"
-  define p q where "p = fst \<circ> pq" and "q = snd \<circ> pq"
+  define pq where "pq \<equiv> (\<lambda>k. quotient_of (\<Sum>i=0..k. of_int (b i) / of_int (a i)))"
+  define p q where "p \<equiv> fst \<circ> pq" and "q = snd \<circ> pq"
   have coprime_pq:"coprime (p k) (q k)"
         and q_pos:"q k > 0" and pq_sum:"p k / q k = (\<Sum>i=0..k. b i / a i)" for k
   proof -
     have eq: "quotient_of (\<Sum>i=0..k. of_int (b i) / of_int (a i)) = (p k, q k)"
       by (simp add: p_def q_def pq_def)
     from quotient_of_coprime[OF eq] show "coprime (p k) (q k)" .
     from quotient_of_denom_pos[OF eq] show "q k > 0" .
     have "(\<Sum>i=0..k. b i / a i) = of_rat (\<Sum>i=0..k. of_int (b i) / of_int (a i))"
       by (simp add: of_rat_sum of_rat_divide)
     also have "(\<Sum>i=0..k. rat_of_int (b i) / rat_of_int (a i)) =
                  rat_of_int (p k) / rat_of_int (q k)"
       using quotient_of_div[OF eq] by simp
     finally show "p k / q k = (\<Sum>i=0..k. b i / a i)" by (simp add:of_rat_divide)
   qed
 
   have \<xi>_Inf_many:"\<exists>\<^sub>\<infinity> k. \<bar>\<xi> - p k / q k\<bar> <  1 / q k powr (2 + \<delta> * \<epsilon> / (1 + \<epsilon>))"
   proof -
     have *:"\<exists>\<^sub>\<infinity>k. (bb (Suc k) / aa (Suc k)) powr (\<epsilon> / (1 + \<epsilon>))
               < \<epsilon> / (2 * prod aa {0..k} powr (2 + \<delta> * \<epsilon> / (1 + \<epsilon>)))"
       using 7[of "(2 / \<epsilon>) powr ((1+\<epsilon>)/ \<epsilon>)"] \<open>\<epsilon>>0\<close> 
       by (auto simp:powr_powr)
     have **:"\<forall>\<^sub>\<infinity>k. \<bar>\<xi> - (\<Sum>k = 0..k. bb k / aa k)\<bar>
                 < 2 / \<epsilon> * (bb (k + 1) / aa (k + 1)) powr (\<epsilon> / (1 + \<epsilon>))"
       using 10[unfolded cofinite_eq_sequentially[symmetric]] .
     from INFM_conjI[OF * **] show ?thesis 
     proof (elim INFM_mono)
       fix k assume asm:"(bb (Suc k) / aa (Suc k)) powr (\<epsilon> / (1 + \<epsilon>))
                          < \<epsilon> / (2 * prod aa {0..k} powr (2 + \<delta> * \<epsilon> / (1 + \<epsilon>))) \<and>
                           \<bar>\<xi> - (\<Sum>k = 0..k. bb k / aa k)\<bar> 
                         < 2 / \<epsilon> * (bb (k + 1) / aa (k + 1)) powr (\<epsilon> / (1 + \<epsilon>))"
       have "\<bar>\<xi> - real_of_int (p k) / real_of_int (q k)\<bar> 
               = \<bar>\<xi> - (\<Sum>k = 0..k. bb k / aa k)\<bar>"
         using pq_sum unfolding aa_def bb_def by auto
       also have "... < (2 / \<epsilon>) * (bb (k+1) / aa (k+1)) powr (\<epsilon> / (1+\<epsilon>))"
         using asm by auto
       also have "... <  (2 / \<epsilon>) * (\<epsilon> / (2 * prod aa {0..k} powr (2 + \<delta> * \<epsilon> / (1 + \<epsilon>))))"
         apply (rule mult_strict_left_mono)
         using asm \<open>\<epsilon>>0\<close> by auto
       also have "... = 1/ prod aa {0..k} powr (2 + \<delta> * \<epsilon> / (1 + \<epsilon>))"
         using \<open>\<epsilon>>0\<close> by auto
       also have "... \<le> 1 / q k powr (2 + \<delta> * \<epsilon> / (1 + \<epsilon>))"
       proof -
         have "q k \<le> prod aa {0..k}"
         proof (induct k)
           case 0
           then show ?case unfolding q_def pq_def aa_def 
             apply (simp add:rat_divide_code of_int_rat quotient_of_Fract)
             using aa_bb_pos[of 0,unfolded aa_def bb_def] unfolding Let_def normalize_def 
             apply auto
             by (metis div_by_1 less_imp_le less_trans nonneg1_imp_zdiv_pos_iff 
                 not_less zdiv_mono2)  
         next
           case (Suc k)
-          define de where "de=snd \<circ> quotient_of"
+          define de where "de \<equiv> snd \<circ> quotient_of"
           have "real_of_int (q (Suc k)) 
                   = de (\<Sum>i=0..Suc k. of_int (b i) / of_int (a i))"
             unfolding q_def pq_def de_def by simp
           also have "... = de ((\<Sum>i=0..k. of_int (b i) / of_int (a i)) 
                                 + of_int (b (Suc k)) / of_int (a (Suc k)))"
             by simp
           also have "... \<le> de (\<Sum>i=0..k. of_int (b i) / of_int (a i)) 
                                 * de (of_int (b (Suc k)) / of_int (a (Suc k)))"          
             using snd_quotient_plus_leq[folded de_def] by presburger
           also have "... = q k * de (of_int (b (Suc k)) / of_int (a (Suc k)))"
             unfolding q_def pq_def de_def by auto
           also have "... = q k * snd (Rat.normalize (b (Suc k), a (Suc k)))"
             by (simp add:rat_divide_code of_int_rat quotient_of_Fract de_def)
           also have "... \<le> q k * aa (Suc k)"
             using aa_bb_pos[of "Suc k"] q_pos[of "k"] 
             unfolding normalize_def aa_def bb_def Let_def
             apply auto
             by (metis div_by_1 int_one_le_iff_zero_less less_trans 
                   nonneg1_imp_zdiv_pos_iff not_less zdiv_mono2 zero_less_one)
           also have "... \<le>  prod aa {0..k} * aa (Suc k)"
             using Suc aa_bb_pos[of "Suc k"] by auto
           also have "... = prod aa {0..Suc k}"
             by (simp add: prod.atLeast0_atMost_Suc)
           finally show ?case .
         qed 
         then show ?thesis
           apply (rule_tac divide_left_mono)
           apply (rule powr_mono2)
           using \<open>\<delta>>0\<close> \<open>\<epsilon>>0\<close> q_pos[of k] 
            apply (auto simp:powr_mult[symmetric])
           by (metis aa_bb_pos(1) less_irrefl)
       qed 
       finally show "\<bar>\<xi> -  p k / q k\<bar> < 1 /  q k powr (2 + \<delta> * \<epsilon> / (1 + \<epsilon>))" .
     qed
   qed
 
-  define pqs where "pqs={(p, q). q>0 \<and> coprime p q \<and> \<bar>\<xi> - real_of_int p / real_of_int q\<bar> 
+  define pqs where "pqs \<equiv> {(p, q). q>0 \<and> coprime p q \<and> \<bar>\<xi> - real_of_int p / real_of_int q\<bar> 
                   < 1 / q powr (2 + \<delta> * \<epsilon> / (1 + \<epsilon>))}"
   have \<xi>_infinite:"infinite pqs"
   proof -
-    define A where "A={k. \<bar>\<xi> -  (p k) /  (q k)\<bar> < 1 / (q k) powr (2 + \<delta> * \<epsilon> / (1 + \<epsilon>))}" 
+    define A where "A \<equiv> {k. \<bar>\<xi> -  (p k) /  (q k)\<bar> < 1 / (q k) powr (2 + \<delta> * \<epsilon> / (1 + \<epsilon>))}" 
     note \<xi>_Inf_many
     then have "infinite A"
       unfolding Inf_many_def A_def by auto
     moreover have "inj_on (\<lambda>k. (p k, q k)) A"
     proof -
-      define g where "g=(\<lambda>i. rat_of_int (b i) / rat_of_int (a i))"
-      define f where "f=(\<lambda>k. \<Sum>i = 0..k. g i)"
+      define g where "g \<equiv> (\<lambda>i. rat_of_int (b i) / rat_of_int (a i))"
+      define f where "f \<equiv> (\<lambda>k. \<Sum>i = 0..k. g i)"
       have g_pos:"g i>0" for i
         unfolding g_def by (simp add: a_pos b_pos)
       have "strict_mono f" unfolding strict_mono_def f_def
       proof safe
         fix x y::nat assume "x < y"
         then have "sum g {0..y} - sum g {0..x} = sum g {x<..y}" 
           apply (subst  Groups_Big.sum_diff[symmetric])
           by (auto intro:arg_cong2[where f=sum])
         also have "... > 0"
           apply (rule ordered_comm_monoid_add_class.sum_pos)
           using \<open>x<y\<close> g_pos by auto
         finally have "sum g {0..y} - sum g {0..x} >0" .
         then show "sum g {0..x} < sum g {0..y}" by auto
       qed
       then have "inj f" using strict_mono_imp_inj_on by auto
       then have "inj (quotient_of o f)" by (simp add: inj_compose quotient_of_inj)
       then have "inj (\<lambda>k. (p k, q k))"
         unfolding f_def p_def q_def pq_def comp_def
         apply (fold g_def)
         by auto
       then show ?thesis by (auto elim:subset_inj_on)
     qed
     moreover have "(\<lambda>k. (p k, q k)) ` A \<subseteq> pqs"
       unfolding A_def pqs_def using coprime_pq q_pos by auto
     ultimately show ?thesis
       apply (elim infinite_inj_imageE)
       by auto
   qed
   moreover have "finite pqs" if "\<xi> \<in> \<rat>"
   proof -
     obtain m n where \<xi>_mn:"\<xi> = (of_int m / of_int n)" and "coprime m n" "n>0"
     proof -
       obtain m n where mn:"\<bar>\<xi>\<bar> = (of_nat m / of_nat n)" "coprime m n" "n\<noteq>0"
         using Rats_abs_nat_div_natE[OF \<open>\<xi> \<in> \<rat>\<close> Rats_abs_nat_div_natE]
         by metis
       define m' and n'::int 
         where "m'=(if \<xi> > 0 then nat m else -nat m)" and "n'=nat n"
       then have "\<xi> = (of_int m' / of_int n')" "coprime m' n'" "n'>0"
         using mn by auto
       then show ?thesis using that by auto
     qed
     have "pqs \<subseteq> {(m,n)} \<union> {x. x \<in>pqs \<and> - \<bar>m\<bar> - 1 \<le>fst x \<and> fst x \<le> \<bar>m\<bar> + 1 \<and> 0<snd x \<and> snd x < n }"
     proof (rule subsetI)
       fix x assume "x \<in> pqs"
-      define p q where "p=fst x" and "q=snd x"
+      define p q where "p \<equiv> fst x" and "q=snd x"
       have "q>0" "coprime p q" and pq_less:"\<bar>\<xi> - p / q\<bar> 
           < 1 / q powr (2 + \<delta> * \<epsilon> / (1 + \<epsilon>))"
         using \<open>x\<in>pqs\<close> unfolding p_def q_def pqs_def by auto
       have q_lt_n:"q<n" when "m\<noteq>p \<or> n\<noteq>q" 
       proof -
         have "m * q \<noteq> n * p" using that \<open>coprime m n\<close> \<open>coprime p q\<close> \<open>q>0\<close> \<open>n>0\<close> 
           by (metis eq_rat(1) fst_conv int_one_le_iff_zero_less mult.commute normalize_stable 
                 not_one_le_zero quotient_of_Fract snd_conv)
         then have "1/(n*q) \<le> \<bar>m/n - p/q\<bar>"
           using \<open>q>0\<close> \<open>n>0\<close>  
           apply (auto simp:field_simps)
           by (metis add_diff_cancel_left' diff_diff_eq2 diff_zero less_irrefl not_le of_int_diff 
                 of_int_lessD of_int_mult)
         also have "...  < 1 / q powr (2 + \<delta> * \<epsilon> / (1 + \<epsilon>))"
           using pq_less unfolding \<xi>_mn by auto
         also have "... \<le> 1 / q ^2"
         proof -
           have "real_of_int (q\<^sup>2) = q powr 2"
             apply (subst powr_numeral)
             unfolding power2_eq_square using \<open>q>0\<close> by auto
           also have "... \<le> q powr (2 + \<delta> * \<epsilon> / (1 + \<epsilon>))"
             apply (rule powr_mono)
             using \<open>q>0\<close> \<open>\<delta>>0\<close> \<open>\<epsilon>>0\<close> by auto
           finally have "real_of_int (q\<^sup>2) 
                           \<le> real_of_int q powr (2 + \<delta> * \<epsilon> / (1 + \<epsilon>))" .
           moreover have "real_of_int q powr (2 + \<delta> * \<epsilon> / (1 + \<epsilon>)) > 0" using \<open>0 < q\<close> by auto
           ultimately show ?thesis by (auto simp:field_simps)
         qed 
         finally have " 1 /  (n * q) < 1 / q\<^sup>2" .
         then show ?thesis  using \<open>q>0\<close> \<open>n>0\<close> 
           unfolding power2_eq_square by (auto simp:field_simps)
       qed
       moreover have "- \<bar>m\<bar> - 1 \<le> p \<and> p \<le> \<bar>m\<bar> + 1" when "m\<noteq>p \<or> n\<noteq>q" 
       proof -
-        define qn where "qn=q/n"
+        define qn where "qn \<equiv> q/n"
         have "0<qn" "qn<1" unfolding qn_def using q_lt_n[OF \<open>m\<noteq>p \<or> n\<noteq>q\<close>] \<open>q>0\<close> by auto
 
         have "\<bar>m/n - p / q\<bar> < 1 / q powr (2 + \<delta> * \<epsilon> / (1 + \<epsilon>))" 
           using pq_less unfolding \<xi>_mn by simp
         then have "\<bar>p / q - m/n\<bar> < 1 / q powr (2 + \<delta> * \<epsilon> / (1 + \<epsilon>))" by simp
         then have " m/n- 1 / q powr (2 + \<delta> * \<epsilon> / (1 + \<epsilon>)) 
             < p/q \<and> p/q < m/n + 1 / q powr (2 + \<delta> * \<epsilon> / (1 + \<epsilon>))"
           unfolding abs_diff_less_iff by auto
         then have "qn*m- q / q powr (2 + \<delta> * \<epsilon> / (1 + \<epsilon>)) < p 
             \<and> p < qn*m + q / q powr (2 + \<delta> * \<epsilon> / (1 + \<epsilon>))"
           unfolding qn_def using \<open>q>0\<close> by (auto simp:field_simps)
         moreover have "- \<bar>m\<bar> - 1 \<le> qn*m- q / q powr (2 + \<delta> * \<epsilon> / (1 + \<epsilon>))"
         proof -
           have "- \<bar>m\<bar> \<le> qn*m" using \<open>0<qn\<close> \<open>qn<1\<close> 
-            apply (cases "m\<ge>0")
-            subgoal 
-              apply simp 
-              by (meson less_eq_real_def mult_nonneg_nonneg neg_le_0_iff_le of_int_0_le_iff 
-                          order_trans)
-            subgoal by simp
-            done
+            apply (simp add: abs_if)
+            by (smt (verit, best) mult_nonneg_nonneg of_int_nonneg)
           moreover have "- 1 \<le> - q / q powr (2 + \<delta> * \<epsilon> / (1 + \<epsilon>))" 
           proof -
             have "q = q powr 1" using \<open>0 < q\<close> by auto
             also have "... \<le>q powr (2 + \<delta> * \<epsilon> / (1 + \<epsilon>))"
               apply (rule powr_mono)
               using \<open>q>0\<close> \<open>\<delta>>0\<close> \<open>\<epsilon>>0\<close> by auto
             finally have "q \<le> q powr (2 + \<delta> * \<epsilon> / (1 + \<epsilon>))" .
             then show ?thesis using \<open>0 < q\<close> by auto
           qed
           ultimately show ?thesis by auto
         qed
         moreover have "qn*m + q / q powr (2 + \<delta> * \<epsilon> / (1 + \<epsilon>)) \<le> \<bar>m\<bar> + 1"
         proof -
           have "qn*m \<le> \<bar>m\<bar>" using \<open>0<qn\<close> \<open>qn<1\<close> 
-            apply (cases "m\<ge>0")
-            subgoal by (simp add: mult_left_le_one_le)
-            subgoal by (smt of_int_0_le_iff zero_le_mult_iff)
-            done
+            apply (simp add: abs_if mult_left_le_one_le)
+            by (meson less_eq_real_def mult_pos_neg neg_0_less_iff_less of_int_less_0_iff order_trans)
           moreover have "q / q powr (2 + \<delta> * \<epsilon> / (1 + \<epsilon>)) \<le> 1"
           proof -
             have "q = q powr 1" using \<open>0 < q\<close> by auto
             also have "... \<le>q powr (2 + \<delta> * \<epsilon> / (1 + \<epsilon>))"
               apply (rule powr_mono)
               using \<open>q>0\<close> \<open>\<delta>>0\<close> \<open>\<epsilon>>0\<close> by auto
             finally have "q \<le> q powr (2 + \<delta> * \<epsilon> / (1 + \<epsilon>))" .
             then show ?thesis using \<open>0 < q\<close> by auto
           qed
           ultimately show ?thesis by auto
         qed
         ultimately show ?thesis by auto
       qed
       ultimately show "x \<in> {(m, n)} \<union> {x \<in> pqs. - \<bar>m\<bar> - 1 \<le> fst x \<and> fst x \<le> \<bar>m\<bar> + 1 
                           \<and> 0 < snd x \<and> snd x < n}" 
         using \<open>x \<in> pqs\<close> \<open>q>0\<close> unfolding p_def q_def by force
     qed
     moreover have "finite {x. x \<in>pqs \<and> - \<bar>m\<bar> - 1 \<le>fst x \<and> fst x \<le> \<bar>m\<bar> + 1 \<and> 0<snd x \<and> snd x < n }" 
     proof -
       have "finite ({- \<bar>m\<bar> - 1..\<bar>m\<bar> +1} \<times> {0<..<n})" by blast
       moreover have "{x. x \<in>pqs \<and> - \<bar>m\<bar> - 1 \<le>fst x \<and> fst x \<le> \<bar>m\<bar> + 1 \<and> 0<snd x \<and> snd x < n } \<subseteq> 
                 ({- \<bar>m\<bar> - 1..\<bar>m\<bar> +1} \<times> {0<..<n})"
         by auto
       ultimately show ?thesis 
-        apply (elim rev_finite_subset)
-        by blast
+        using finite_subset by blast
     qed
     ultimately show ?thesis using finite_subset by auto
   qed
   ultimately show ?thesis 
     apply (fold \<xi>_def)
     using RothsTheorem[rule_format,of \<xi> "2 + \<delta> * \<epsilon> / (1 + \<epsilon>)",folded pqs_def] 
       \<open>\<delta> >0\<close> \<open>\<epsilon>>0\<close> 
     apply (auto simp:divide_simps )
     by (meson mult_le_0_iff not_less)
 qed
 
 subsection\<open> Acknowledgements\<close>
 
 text\<open>A.K.-A. and W.L. were supported by the ERC Advanced Grant ALEXANDRIA (Project 742178)
  funded by the European Research Council and led by Professor Lawrence Paulson
  at the University of Cambridge, UK. Thanks to Iosif Pinelis for his clarification on
 MathOverflow regarding the summmability of the series in @{thm [source] RothsTheorem.HanclRucki2}
 @{url "https://mathoverflow.net/questions/323069/why-is-this-series-summable"}
 and to Manuel Eberl for his helpful comments.\<close>
 
 end
\ No newline at end of file