src/HOL/Analysis/Cauchy_Integral_Theorem.thy

 by (auto simp: vector_derivative_circlepath norm_mult intro: contour_integral_uniform_limit assms)
 
 
 subsection\<open> General stepping result for derivative formulas.\<close>
 
-lemma sum_sqs_eq:
-  fixes x::"'a::idom" shows "x * x + y * y = x * (y * 2) \<Longrightarrow> y = x"
-  by algebra
-
 proposition Cauchy_next_derivative:
   assumes "continuous_on (path_image \<gamma>) f'"
       and leB: "\<And>t. t \<in> {0..1} \<Longrightarrow> norm (vector_derivative \<gamma> (at t)) \<le> B"
       and int: "\<And>w. w \<in> s - path_image \<gamma> \<Longrightarrow> ((\<lambda>u. f' u / (u - w)^k) has_contour_integral f w) \<gamma>"
       and k: "k \<noteq> 0"