src/HOL/Computational_Algebra/Fundamental_Theorem_Algebra.thy

 
 lemma metric_bound_lemma: "cmod (x - y) \<le> \<bar>Re x - Re y\<bar> + \<bar>Im x - Im y\<bar>"
   using real_sqrt_sum_squares_triangle_ineq[of "Re x - Re y" 0 0 "Im x - Im y"]
   unfolding cmod_def by simp
 
-lemma bolzano_weierstrass_complex_disc:
+lemma Bolzano_Weierstrass_complex_disc:
   assumes r: "\<forall>n. cmod (s n) \<le> r"
   shows "\<exists>f z. strict_mono (f :: nat \<Rightarrow> nat) \<and> (\<forall>e >0. \<exists>N. \<forall>n \<ge> N. cmod (s (f n) - z) < e)"
 proof -
   from seq_monosub[of "Re \<circ> s"]
   obtain f where f: "strict_mono f" "monoseq (\<lambda>n. Re (s (f n)))"

       using s1[rule_format, of "?m + 1/real (Suc n)"] by simp
     then have th: "\<forall>n. \<exists>z. cmod z \<le> r \<and> cmod (poly p z) < - s + 1 / real (Suc n)" ..
     from choice[OF th] obtain g where
         g: "\<forall>n. cmod (g n) \<le> r" "\<forall>n. cmod (poly p (g n)) <?m + 1 /real(Suc n)"
       by blast
-    from bolzano_weierstrass_complex_disc[OF g(1)]
+    from Bolzano_Weierstrass_complex_disc[OF g(1)]
     obtain f z where fz: "strict_mono (f :: nat \<Rightarrow> nat)" "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. cmod (g (f n) - z) < e"
       by blast
     {
       fix w
       assume wr: "cmod w \<le> r"