src/HOL/Analysis/Cauchy_Integral_Theorem.thy

       case le show ?diff_fg
       proof (rule differentiable_transform_within [where d = "dist x c" and f = f])
         have "f differentiable at x within ({a<..<c} - s)"
           apply (rule differentiable_at_withinI)
           using x le st
-          by (metis (no_types, lifting) DiffD1 DiffD2 DiffI UnCI atLeastAtMost_diff_ends atLeastAtMost_iff at_within_interior insert_iff interior_atLeastAtMost le st(3) x)
+          by (metis (no_types, lifting) DiffD1 DiffD2 DiffI UnCI atLeastAtMost_diff_ends atLeastAtMost_iff at_within_interior insert_iff interior_atLeastAtMost_real le st(3) x)
         moreover have "open ({a<..<c} - s)"
           by (blast intro: open_greaterThanLessThan \<open>finite s\<close> finite_imp_closed)
         ultimately show "f differentiable at x within {a..b}"
           using x le by (auto simp add: at_within_open_NO_MATCH differentiable_at_withinI)
       qed (use x le st dist_real_def in auto)

       case ge show ?diff_fg
       proof (rule differentiable_transform_within [where d = "dist x c" and f = g])
         have "g differentiable at x within ({c<..<b} - t)"
           apply (rule differentiable_at_withinI)
           using x ge st
-          by (metis DiffD1 DiffD2 DiffI UnCI atLeastAtMost_diff_ends atLeastAtMost_iff at_within_interior insert_iff interior_atLeastAtMost)
+          by (metis DiffD1 DiffD2 DiffI UnCI atLeastAtMost_diff_ends atLeastAtMost_iff at_within_interior insert_iff interior_atLeastAtMost_real)
         moreover have "open ({c<..<b} - t)"
           by (blast intro: open_greaterThanLessThan \<open>finite t\<close> finite_imp_closed)
         ultimately show "g differentiable at x within {a..b}"
           using x ge by (auto simp add: at_within_open_NO_MATCH differentiable_at_withinI)
       qed (use x ge st dist_real_def in auto)

       by (simp add: has_vector_derivative_def scaleR_conv_of_real o_def mult_ac)
   } note * = this
   show ?thesis
     apply (rule fundamental_theorem_of_calculus_interior_strong)
     using k assms cfg *
-    apply (auto simp: at_within_closed_interval)
+    apply (auto simp: at_within_Icc_at)
     done
 qed
 
 lemma contour_integral_primitive:
   assumes "\<And>x. x \<in> s \<Longrightarrow> (f has_field_derivative f' x) (at x within s)"

     by (auto simp: open_dist)
 qed
 
 subsection\<open>Winding number is zero "outside" a curve, in various senses\<close>
 
-lemma winding_number_zero_in_outside:
+proposition winding_number_zero_in_outside:
   assumes \<gamma>: "path \<gamma>" and loop: "pathfinish \<gamma> = pathstart \<gamma>" and z: "z \<in> outside (path_image \<gamma>)"
     shows "winding_number \<gamma> z = 0"
 proof -
   obtain B::real where "0 < B" and B: "path_image \<gamma> \<subseteq> ball 0 B"
     using bounded_subset_ballD [OF bounded_path_image [OF \<gamma>]] by auto

       by (auto intro: winding_number_unique [OF \<gamma>] simp add: wnot)
   qed
   finally show ?thesis .
 qed
 
-lemma winding_number_zero_outside:
+corollary winding_number_zero_const: "a \<noteq> z \<Longrightarrow> winding_number (\<lambda>t. a) z = 0"
+  by (rule winding_number_zero_in_outside)
+     (auto simp: pathfinish_def pathstart_def path_polynomial_function)
+
+corollary winding_number_zero_outside:
     "\<lbrakk>path \<gamma>; convex s; pathfinish \<gamma> = pathstart \<gamma>; z \<notin> s; path_image \<gamma> \<subseteq> s\<rbrakk> \<Longrightarrow> winding_number \<gamma> z = 0"
   by (meson convex_in_outside outside_mono subsetCE winding_number_zero_in_outside)
 
 lemma winding_number_zero_at_infinity:
   assumes \<gamma>: "path \<gamma>" and loop: "pathfinish \<gamma> = pathstart \<gamma>"