Theory Cauchy_Index_Theorem

theory Cauchy_Index_Theorem
imports Missing_Transcendental Missing_Analysis
(*
    Author:     Wenda Li <wl302@cam.ac.uk / liwenda1990@hotmail.com>
*)

section ‹Cauchy's index theorem›

theory Cauchy_Index_Theorem imports 
  "HOL-Complex_Analysis.Complex_Analysis"
  "Sturm_Tarski.Sturm_Tarski"
  "HOL-Computational_Algebra.Fundamental_Theorem_Algebra"
  Missing_Transcendental
  Missing_Algebraic
  Missing_Analysis
begin

text ‹This theory formalises Cauchy indices on the complex plane and relate them to winding numbers›

subsection ‹Misc›
  
(*refined version of the library one with the same name by dropping unnecessary assumptions*) 
lemma atMostAtLeast_subset_convex:
  fixes C :: "real set"
  assumes "convex C"
    and "x ∈ C" "y ∈ C" 
  shows "{x .. y} ⊆ C"
proof safe
  fix z assume z: "z ∈ {x .. y}"
  have "z ∈ C" if *: "x < z" "z < y"
  proof -
    let  = "(y - z) / (y - x)"
    have "0 ≤ ?μ" "?μ ≤ 1"
      using assms * by (auto simp: field_simps)
    then have comb: "?μ * x + (1 - ?μ) * y ∈ C"
      using assms iffD1[OF convex_alt, rule_format, of C y x ]
      by (simp add: algebra_simps)
    have "?μ * x + (1 - ?μ) * y = (y - z) * x / (y - x) + (1 - (y - z) / (y - x)) * y"
      by (auto simp: field_simps)
    also have "… = ((y - z) * x + (y - x - (y - z)) * y) / (y - x)"
      using * by (simp only: add_divide_distrib) (auto simp: field_simps)
    also have "… = z"
      using assms * by (auto simp: field_simps)
    finally show ?thesis
      using comb by auto
  qed
  then show "z ∈ C"
    using z assms by (auto simp: le_less)
qed
  
lemma arg_elim:
  "f x ⟹ x= y ⟹ f y"
  by auto
 
lemma arg_elim2:
  "f x1 x2 ⟹ x1= y1 ⟹x2=y2 ⟹ f y1 y2"
  by auto
 
lemma arg_elim3:
  "⟦f x1 x2 x3;x1= y1;x2=y2;x3=y3 ⟧ ⟹ f y1 y2 y3"
  by auto  
    
lemma IVT_strict:
  fixes f :: "'a::linear_continuum_topology ⇒ 'b::linorder_topology"
  assumes "(f a > y ∧ y > f b) ∨ (f a < y ∧ y < f b)" "a<b" "continuous_on {a .. b} f"
  shows "∃x. a < x ∧ x < b ∧ f x = y"
by (metis IVT' IVT2' assms(1) assms(2) assms(3) linorder_neq_iff order_le_less order_less_imp_le)    
  
lemma (in dense_linorder) atLeastAtMost_subseteq_greaterThanLessThan_iff:
  "{a .. b} ⊆ { c <..< d } ⟷ (a ≤ b ⟶ c < a ∧ b < d)"
  using dense[of "a" "min c b"] dense[of "max a d" "b"]
  by (force simp: subset_eq Ball_def not_less[symmetric])    

lemma Re_winding_number_half_right:
  assumes "∀p∈path_image γ. Re p ≥ Re z" and "valid_path γ" and  "z∉path_image γ"
  shows "Re(winding_number γ z) = (Im (Ln (pathfinish γ - z)) - Im (Ln (pathstart γ - z)))/(2*pi)"
proof -
  define g where "g=(λt. γ t - z)"
  define st fi where "st≡pathstart g" and "fi≡pathfinish g"
  have "valid_path g" "0∉path_image g" and pos_img:"∀p∈path_image g. Re p ≥ 0" unfolding g_def 
    subgoal using assms(2) by auto
    subgoal using assms(3) by auto
    subgoal using assms(1) by fastforce
    done
  have "(inverse has_contour_integral Ln fi - Ln st) g"
    unfolding fi_def st_def
  proof (rule contour_integral_primitive[OF _ ‹valid_path g›,of " - ℝ0"])
    fix x::complex assume "x ∈ - ℝ0"
    then have "(Ln has_field_derivative inverse x) (at x)" using has_field_derivative_Ln
      by auto
    then show "(Ln has_field_derivative inverse x) (at x within - ℝ0)"
      using has_field_derivative_at_within by auto
  next
    show "path_image g ⊆ - ℝ0" using pos_img ‹0∉path_image g›
      by (metis ComplI antisym assms(3) complex_nonpos_Reals_iff complex_surj
          subsetI zero_complex.code)
  qed
  then have winding_eq:"2*pi*𝗂*winding_number g 0 = (Ln fi - Ln st)"
    using has_contour_integral_winding_number[OF ‹valid_path g› ‹0∉path_image g›
        ,simplified,folded inverse_eq_divide] has_contour_integral_unique 
    by auto
  have "Re(winding_number g 0) 
      = (Im (Ln fi) - Im (Ln st))/(2*pi)"
    (is "?L=?R")
  proof -
    have "?L = Re((Ln fi - Ln st)/(2*pi*𝗂))"
      using winding_eq[symmetric] by auto
    also have "... = ?R"
      by (metis Im_divide_of_real Im_i_times complex_i_not_zero minus_complex.simps(2) 
          mult.commute mult_divide_mult_cancel_left_if times_divide_eq_right)
    finally show ?thesis .
  qed
  then show ?thesis unfolding g_def fi_def st_def using winding_number_offset by simp
qed      
  
lemma Re_winding_number_half_upper:
  assumes pimage:"∀p∈path_image γ. Im p ≥ Im z" and "valid_path γ" and "z∉path_image γ"
  shows "Re(winding_number γ z) = 
            (Im (Ln (𝗂*z - 𝗂*pathfinish γ)) - Im (Ln (𝗂*z - 𝗂*pathstart γ )))/(2*pi)"
proof -
  define γ' where "γ'=(λt. - 𝗂 * (γ t - z) + z)"
  have "Re (winding_number γ' z) = (Im (Ln (pathfinish γ' - z)) - Im (Ln (pathstart γ' - z))) / (2 * pi)"
    unfolding γ'_def
    apply (rule Re_winding_number_half_right)
    subgoal using pimage unfolding path_image_def by auto
    subgoal 
      apply (rule valid_path_compose_holomorphic[OF ‹valid_path γ›,of "λx. -𝗂 * (x-z) + z" UNIV
            , unfolded comp_def])
      by (auto intro!:holomorphic_intros)
    subgoal using ‹z∉path_image γ› unfolding path_image_def by auto
    done
  moreover have "winding_number γ' z = winding_number γ z"
  proof -
    define f where "f=(λx. -𝗂 * (x-z) + z)"
    define c where "c= 1 / (complex_of_real (2 * pi) * 𝗂)"
    have "winding_number γ' z = winding_number (f o γ) z" 
      unfolding γ'_def comp_def f_def by auto
    also have "... = c * contour_integral γ (λw. deriv f w / (f w - z))" unfolding c_def
    proof (rule winding_number_comp[of UNIV])
      show "z ∉ path_image (f ∘ γ)" using ‹z∉path_image γ› unfolding f_def path_image_def by auto
    qed (auto simp add:f_def ‹valid_path γ› intro!:holomorphic_intros)
    also have "... = c * contour_integral γ (λw.  1 / (w - z))"
    proof -
      have "deriv f x = -𝗂" for x
        unfolding f_def
        by (auto intro!:derivative_eq_intros DERIV_imp_deriv)
      then show ?thesis    
        unfolding f_def c_def 
        by (auto simp add:field_simps divide_simps intro!:arg_cong2[where f=contour_integral])
    qed
    also have "... = winding_number γ z"
      using winding_number_valid_path[OF ‹valid_path γ› ‹z∉path_image γ›,folded c_def] by simp
    finally show ?thesis .
  qed    
  moreover have "pathfinish γ' = z+ 𝗂*z -𝗂* pathfinish γ" "pathstart γ' = z+ 𝗂*z -𝗂*pathstart γ"  
    unfolding γ'_def path_defs by (auto simp add:algebra_simps)
  ultimately show ?thesis by auto
qed
    
lemma Re_winding_number_half_lower:
  assumes pimage:"∀p∈path_image γ. Im p ≤ Im z" and "valid_path γ" and "z∉path_image γ"
  shows "Re(winding_number γ z) = 
             (Im (Ln ( 𝗂*pathfinish γ - 𝗂*z)) - Im (Ln (𝗂*pathstart γ - 𝗂*z)))/(2*pi)"
proof -
  define γ' where "γ'=(λt. 𝗂 * (γ t - z) + z)"
  have "Re (winding_number γ' z) = (Im (Ln (pathfinish γ' - z)) - Im (Ln (pathstart γ' - z))) / (2 * pi)"
    unfolding γ'_def
    apply (rule Re_winding_number_half_right)
    subgoal using pimage unfolding path_image_def by auto
    subgoal 
      apply (rule valid_path_compose_holomorphic[OF ‹valid_path γ›,of "λx. 𝗂 * (x-z) + z" UNIV
            , unfolded comp_def])
      by (auto intro!:holomorphic_intros)
    subgoal using ‹z∉path_image γ› unfolding path_image_def by auto
    done
  moreover have "winding_number γ' z = winding_number γ z"
  proof -
    define f where "f=(λx. 𝗂 * (x-z) + z)"
    define c where "c= 1 / (complex_of_real (2 * pi) * 𝗂)"
    have "winding_number γ' z = winding_number (f o γ) z" 
      unfolding γ'_def comp_def f_def by auto
    also have "... = c * contour_integral γ (λw. deriv f w / (f w - z))" unfolding c_def
    proof (rule winding_number_comp[of UNIV])
      show "z ∉ path_image (f ∘ γ)" using ‹z∉path_image γ› unfolding f_def path_image_def by auto
    qed (auto simp add:f_def ‹valid_path γ› intro!:holomorphic_intros)
    also have "... = c * contour_integral γ (λw.  1 / (w - z))"
    proof -
      have "deriv f x = 𝗂" for x
        unfolding f_def
        by (auto intro!:derivative_eq_intros DERIV_imp_deriv)
      then show ?thesis    
        unfolding f_def c_def 
        by (auto simp add:field_simps divide_simps intro!:arg_cong2[where f=contour_integral])
    qed
    also have "... = winding_number γ z"
      using winding_number_valid_path[OF ‹valid_path γ› ‹z∉path_image γ›,folded c_def] by simp
    finally show ?thesis .
  qed    
  moreover have "pathfinish γ' = z+ 𝗂* pathfinish γ - 𝗂*z" "pathstart γ' = z+ 𝗂*pathstart γ - 𝗂*z"  
    unfolding γ'_def path_defs by (auto simp add:algebra_simps)
  ultimately show ?thesis by auto
qed    
    
      
lemma Re_winding_number_half_left:
  assumes neg_img:"∀p∈path_image γ. Re p ≤ Re z" and "valid_path γ" and "z∉path_image γ"
  shows "Re(winding_number γ z) = (Im (Ln (z - pathfinish γ)) - Im (Ln (z - pathstart γ )))/(2*pi)"
proof -
  define γ' where "γ'≡(λt. 2*z - γ t)"
  have "Re (winding_number γ' z) = (Im (Ln (pathfinish γ' - z)) - Im (Ln (pathstart γ' - z))) / (2 * pi)"
    unfolding γ'_def
    apply (rule Re_winding_number_half_right)
    subgoal using neg_img unfolding path_image_def by auto
    subgoal 
      apply (rule valid_path_compose_holomorphic[OF ‹valid_path γ›,of "λt. 2*z-t" UNIV,
            unfolded comp_def])
      by (auto intro:holomorphic_intros)
    subgoal using ‹z∉path_image γ› unfolding path_image_def by auto
    done
  moreover have "winding_number γ' z = winding_number γ z"
  proof -
    define f where "f=(λt. 2*z-t)"
    define c where "c= 1 / (complex_of_real (2 * pi) * 𝗂)"
    have "winding_number γ' z = winding_number (f o γ) z" 
      unfolding γ'_def comp_def f_def by auto
    also have "... = c * contour_integral γ (λw. deriv f w / (f w - z))" unfolding c_def
    proof (rule winding_number_comp[of UNIV])
      show "z ∉ path_image (f ∘ γ)" using ‹z∉path_image γ› unfolding f_def path_image_def by auto
    qed (auto simp add:f_def ‹valid_path γ› intro:holomorphic_intros)
    also have "... = c * contour_integral γ (λw.  1 / (w - z))" 
      unfolding f_def c_def 
      by (auto simp add:field_simps divide_simps intro!:arg_cong2[where f=contour_integral])
    also have "... = winding_number γ z"
      using winding_number_valid_path[OF ‹valid_path γ› ‹z∉path_image γ›,folded c_def] by simp
    finally show ?thesis .
  qed
  moreover have "pathfinish γ' = 2*z - pathfinish γ" "pathstart γ' = 2*z - pathstart γ"  
    unfolding γ'_def path_defs by auto 
  ultimately show ?thesis by auto    
qed 
  
lemma continuous_on_open_Collect_neq:
  fixes f g :: "'a::topological_space ⇒ 'b::t2_space"
  assumes f: "continuous_on S f" and g: "continuous_on S g" and "open S"
  shows "open {x∈S. f x ≠ g x}"
proof (rule topological_space_class.openI)
  fix t
  assume "t ∈ {x∈S. f x ≠ g x}"
  then obtain U0 V0 where "open U0" "open V0" "f t ∈ U0" "g t ∈ V0" "U0 ∩ V0 = {}" "t∈S"
    by (auto simp add: separation_t2)
  obtain U1 where "open U1" "t ∈ U1" "∀y∈(S ∩ U1). f y ∈ U0"
    using f[unfolded continuous_on_topological,rule_format,OF ‹t∈S› ‹open U0› ‹f t ∈U0›] by auto
  obtain V1 where "open V1" "t ∈ V1" "∀y∈(S ∩ V1). g y ∈ V0"
    using g[unfolded continuous_on_topological,rule_format,OF ‹t∈S› ‹open V0› ‹g t ∈V0›] by auto 
  define T where "T=V1 ∩ U1 ∩ S"
  have "open T" unfolding T_def using ‹open U1› ‹open V1› ‹open S› by auto
  moreover have "t ∈ T" unfolding T_def using ‹t∈U1› ‹t∈V1› ‹t∈S› by auto
  moreover have "T ⊆ {x ∈ S. f x ≠ g x}" unfolding T_def
    using ‹U0 ∩ V0 = {}› ‹∀y∈S ∩ U1. f y ∈ U0› ‹∀y∈S ∩ V1. g y ∈ V0› by auto
  ultimately show "∃T. open T ∧ t ∈ T ∧ T ⊆ {x ∈ S. f x ≠ g x}" by auto
qed  
    
subsection ‹Sign at a filter›    
 
(*Relaxation in types could be done in the future.*)
definition has_sgnx::"(real ⇒ real) ⇒ real ⇒ real filter ⇒ bool" 
    (infixr "has'_sgnx" 55) where
  "(f has_sgnx c) F= (eventually (λx. sgn(f x) = c) F)"    
  
definition sgnx_able (infixr "sgnx'_able" 55) where
  "(f sgnx_able F) = (∃c. (f has_sgnx c) F)"
  
definition sgnx where
  "sgnx f F = (SOME c. (f has_sgnx c) F)"
  
lemma has_sgnx_eq_rhs: "(f has_sgnx x) F ⟹ x = y ⟹ (f has_sgnx y) F"
  by simp

named_theorems sgnx_intros "introduction rules for has_sgnx"
setup ‹
  Global_Theory.add_thms_dynamic (@{binding sgnx_eq_intros},
    fn context =>
      Named_Theorems.get (Context.proof_of context) @{named_theorems sgnx_intros}
      |> map_filter (try (fn thm => @{thm has_sgnx_eq_rhs} OF [thm])))
›  

lemma sgnx_able_sgnx:"f sgnx_able F ⟹ (f has_sgnx (sgnx f F)) F"
  unfolding sgnx_able_def sgnx_def using someI_ex by metis    

lemma has_sgnx_imp_sgnx_able[elim]:
  "(f has_sgnx c) F ⟹ f sgnx_able F"
unfolding sgnx_able_def by auto

lemma has_sgnx_unique:
  assumes "F≠bot" "(f has_sgnx c1) F" "(f has_sgnx c2) F" 
  shows "c1=c2"
proof (rule ccontr)
  assume "c1 ≠ c2 "
  have "eventually (λx. sgn(f x) = c1 ∧ sgn(f x) = c2) F" 
    using assms  unfolding has_sgnx_def eventually_conj_iff by simp
  then have "eventually (λ_. c1 = c2) F" by (elim eventually_mono,auto)
  then have "eventually (λ_. False) F" using ‹c1 ≠ c2› by auto
  then show False using ‹F ≠ bot› eventually_False by auto
qed

lemma has_sgnx_imp_sgnx[elim]:
  "(f has_sgnx c) F ⟹F≠bot ⟹ sgnx f F = c"
  using has_sgnx_unique sgnx_def by auto

lemma has_sgnx_const[simp,sgnx_intros]:
  "((λ_. c) has_sgnx sgn c) F"
by (simp add: has_sgnx_def)

lemma finite_sgnx_at_left_at_right:
  assumes "finite {t. f t=0 ∧ a<t ∧ t<b}" "continuous_on ({a<..<b} - s) f" "finite s" 
      and x:"x∈{a<..<b}"
  shows "f sgnx_able (at_left x)" "sgnx f (at_left x)≠0"
        "f sgnx_able (at_right x)" "sgnx f (at_right x)≠0"
proof -
  define ls where "ls ≡ {t. (f t=0 ∨ t∈s) ∧ a<t ∧t<x }"
  define l where "l≡(if ls = {} then (a+x)/2 else (Max ls + x)/2)" 
  have "finite ls"
  proof -
    have "{t. f t=0 ∧ a<t ∧ t<x} ⊆ {t. f t=0 ∧ a<t ∧ t<b}" using x by auto
    then have "finite {t. f t=0 ∧ a<t ∧ t<x}" using assms(1) 
      using finite_subset by blast
    moreover have "finite {t. t∈s ∧ a<t ∧ t<x}" using assms(3) by auto
    moreover have "ls = {t. f t=0 ∧ a<t ∧ t<x} ∪ {t. t∈s ∧ a<t ∧ t<x}"
      unfolding ls_def by auto
    ultimately show ?thesis by auto
  qed
  have [simp]: "l<x" "a<l" "l<b"
  proof -
    have "l<x ∧ a<l ∧ l<b" when "ls = {}" 
      using that x unfolding l_def by auto
    moreover have "l<x ∧ a<l ∧ l<b" when "ls ≠{}"
    proof -
      have "Max ls ∈ ls" using assms(1,3) that ‹finite ls›
        apply (intro linorder_class.Max_in)
        by auto
      then have "a<Max ls ∧ Max ls < x" unfolding ls_def by auto
      then show ?thesis unfolding l_def using that x by auto
    qed
    ultimately show "l<x" "a<l" "l<b" by auto
  qed  
  have noroot:"f t≠0" when t:"t∈{l..<x}" for t
  proof (cases "ls = {}")
    case True
    have False when "f t=0"
    proof -
      have "t>a" using t ‹l>a› by (meson atLeastLessThan_iff less_le_trans)
      then have "t∈ls" using that t unfolding ls_def by auto
      then show False using True by auto
    qed
    then show ?thesis by auto 
  next
    case False
    have "t>Max ls" using that False ‹l<x› unfolding l_def by auto
    have False when "f t=0" 
    proof -
      have "t>a" using t ‹l>a› by (meson atLeastLessThan_iff less_le_trans)
      then have "t∈ls" using that t unfolding ls_def by auto
      then have "t≤Max ls" using ‹finite ls› by auto
      then show False using ‹t>Max ls› by auto
    qed
    then show ?thesis by auto
  qed
  have "(f has_sgnx sgn (f l)) (at_left x)" unfolding has_sgnx_def
  proof (rule eventually_at_leftI[OF _ ‹l<x›])
    fix t assume t:"t∈{l<..<x}"
    then have [simp]:"t>a" "t<b" using ‹l>a› x 
      by (meson greaterThanLessThan_iff less_trans)+
    have False when "f t = 0" 
      using noroot t that by auto
    moreover have False when "f l=0" 
      using noroot t that by auto
    moreover have False when "f l>0 ∧ f t<0 ∨ f l <0 ∧ f t >0" 
    proof -
      have False when "{l..t} ∩ s ≠{}" 
      proof -
        obtain t' where t':"t'∈{l..t}" "t'∈s" 
          using ‹{l..t} ∩ s ≠ {}› by blast
        then have "a<t' ∧ t'<x" 
          by (metis ‹a < l› atLeastAtMost_iff greaterThanLessThan_iff le_less less_trans t)
        then have "t'∈ls" unfolding ls_def using ‹t'∈s› by auto
        then have "t'≤Max ls" using ‹finite ls› by auto
        moreover have "Max ls<l" 
          using ‹l<x› ‹t'∈ls› ‹finite ls› unfolding l_def by (auto simp add:ls_def )
        ultimately show False using t'(1) by auto
      qed
      moreover have "{l..t} ⊆ {a<..<b}" 
        by (intro atMostAtLeast_subset_convex,auto)
      ultimately have "continuous_on {l..t} f" using assms(2) 
        by (elim continuous_on_subset,auto) 
      then have "∃x>l. x < t ∧ f x = 0"
        apply (intro IVT_strict)
        using that t assms(2) by auto 
      then obtain t' where "l<t'" "t'<t" "f t'=0" by auto
      then have "t'∈{l..<x}" unfolding ls_def using t by auto
      then show False using noroot ‹f t'=0› by auto
    qed
    ultimately show "sgn (f t) = sgn (f l)" 
      by (metis le_less not_less sgn_if)
  qed
  then show "f sgnx_able (at_left x)" by auto   
  show "sgnx f (at_left x)≠0" 
    using noroot[of l,simplified] ‹(f has_sgnx sgn (f l)) (at_left x)›
    by (simp add: has_sgnx_imp_sgnx sgn_if)
next
  define rs where "rs ≡ {t. (f t=0 ∨ t∈s) ∧ x<t ∧ t<b}"
  define r where "r≡(if rs = {} then (x+b)/2 else (Min rs + x)/2)" 
  have "finite rs" 
  proof -
    have "{t. f t=0 ∧ x<t ∧ t<b} ⊆ {t. f t=0 ∧ a<t ∧ t<b}" using x by auto
    then have "finite {t. f t=0 ∧ x<t ∧ t<b}" using assms(1) 
      using finite_subset by blast
    moreover have "finite {t. t∈s ∧ x<t ∧ t<b}" using assms(3) by auto
    moreover have "rs = {t. f t=0 ∧ x<t ∧ t<b} ∪ {t. t∈s ∧ x<t ∧ t<b}"
      unfolding rs_def by auto
    ultimately show ?thesis by auto
  qed  
  
  have [simp]: "r>x" "a<r" "r<b"
  proof -
    have "r>x ∧ a<r ∧ r<b" when "rs = {}" 
      using that x unfolding r_def by auto
    moreover have "r>x ∧ a<r ∧ r<b" when "rs ≠{}"
    proof -
      have "Min rs ∈ rs" using assms(1,3) that ‹finite rs›
        apply (intro linorder_class.Min_in)
        by auto
      then have "x<Min rs ∧ Min rs < b" unfolding rs_def by auto
      then show ?thesis unfolding r_def using that x by auto
    qed
    ultimately show "r>x" "a<r" "r<b" by auto
  qed   
  have noroot:"f t≠0" when t:"t∈{x<..r}" for t
  proof (cases "rs = {}")
    case True
    have False when "f t=0"
    proof -
      have "t<b" using t ‹r<b› 
        using greaterThanAtMost_iff by fastforce 
      then have "t∈rs" using that t unfolding rs_def by auto
      then show False using True by auto
    qed
    then show ?thesis by auto
  next
    case False
    have "t<Min rs" using that False ‹r>x› unfolding r_def by auto
    have False when "f t=0" 
    proof -
      have "t<b" using t ‹r<b› by (metis greaterThanAtMost_iff le_less less_trans)
      then have "t∈rs" using that t unfolding rs_def by auto
      then have "t≥Min rs" using ‹finite rs› by auto
      then show False using ‹t<Min rs› by auto
    qed
    then show ?thesis by auto
  qed
  have "(f has_sgnx sgn (f r)) (at_right x)" unfolding has_sgnx_def
  proof (rule eventually_at_rightI[OF _ ‹r>x›])
    fix t assume t:"t∈{x<..<r}"
    then have [simp]:"t>a" "t<b" using ‹r<b› x 
      by (meson greaterThanLessThan_iff less_trans)+
    have False when "f t = 0" 
      using noroot t that by auto
    moreover have False when "f r=0" 
      using noroot t that by auto
    moreover have False when "f r>0 ∧ f t<0 ∨ f r <0 ∧ f t >0" 
    proof -
      have False when "{t..r} ∩ s ≠{}" 
      proof -
        obtain t' where t':"t'∈{t..r}" "t'∈s" 
          using ‹{t..r} ∩ s ≠ {}› by blast
        then have "x<t' ∧ t'<b" 
          by (meson ‹r < b› atLeastAtMost_iff greaterThanLessThan_iff less_le_trans not_le t)
        then have "t'∈rs" unfolding rs_def using t ‹t'∈s› by auto
        then have "t'≥Min rs" using ‹finite rs› by auto
        moreover have "Min rs>r" 
          using ‹r>x› ‹t'∈rs› ‹finite rs› unfolding r_def by (auto simp add:rs_def )
        ultimately show False using t'(1) by auto
      qed
      moreover have "{t..r} ⊆ {a<..<b}"
        by (intro atMostAtLeast_subset_convex,auto)
      ultimately have "continuous_on {t..r} f" using assms(2) by (elim continuous_on_subset,auto) 
      then have "∃x>t. x < r ∧ f x = 0"
        apply (intro IVT_strict)
        using that t assms(2) by auto
      then obtain t' where "t<t'" "t'<r" "f t'=0" by auto
      then have "t'∈{x<..r}" unfolding rs_def using t by auto
      then show False using noroot ‹f t'=0› by auto
    qed
    ultimately show "sgn (f t) = sgn (f r)" 
      by (metis le_less not_less sgn_if)
  qed
  then show "f sgnx_able (at_right x)" by auto   
  show "sgnx f (at_right x)≠0" 
    using noroot[of r,simplified] ‹(f has_sgnx sgn (f r)) (at_right x)›
    by (simp add: has_sgnx_imp_sgnx sgn_if)    
qed

lemma sgnx_able_poly[simp]:
  "(poly p) sgnx_able (at_right a)"
  "(poly p) sgnx_able (at_left a)"
  "(poly p) sgnx_able at_top"
  "(poly p) sgnx_able at_bot"
proof -
  show "(poly p) sgnx_able at_top"
    using has_sgnx_def poly_sgn_eventually_at_top sgnx_able_def by blast
  show "(poly p) sgnx_able at_bot"
    using has_sgnx_def poly_sgn_eventually_at_bot sgnx_able_def by blast
  show "(poly p) sgnx_able (at_right a)"
  proof (cases "p=0")
    case True
    then show ?thesis unfolding sgnx_able_def has_sgnx_def eventually_at_right
      using linordered_field_no_ub by force
  next
    case False
    obtain ub where "ub>a" and ub:"∀z. a<z∧z≤ub⟶poly p z≠0" 
      using next_non_root_interval[OF False] by auto 
    have "∀z. a<z∧z≤ub⟶sgn(poly p z) = sgn (poly p ub)"
    proof (rule ccontr)
      assume "¬ (∀z. a < z ∧ z ≤ ub ⟶ sgn (poly p z) = sgn (poly p ub))"
      then obtain z where "a<z" "z≤ub" "sgn(poly p z) ≠ sgn (poly p ub)" by auto
      moreover then have "poly p z≠0" "poly p ub≠0" "z≠ub" using ub ‹ub>a› by blast+
      ultimately have "(poly p z>0 ∧ poly p ub<0) ∨ (poly p z<0 ∧ poly p ub>0)"
        by (metis linorder_neqE_linordered_idom sgn_neg sgn_pos)
      then have "∃x>z. x < ub ∧ poly p x = 0" 
        using poly_IVT_neg[of z ub p] poly_IVT_pos[of z ub p] ‹z≤ub› ‹z≠ub› by argo  
      then show False using ub ‹a < z› by auto  
    qed
    then show ?thesis unfolding sgnx_able_def has_sgnx_def eventually_at_right
      apply (rule_tac exI[where x="sgn(poly p ub)"])
      apply (rule_tac exI[where x="ub"])
      using less_eq_real_def ‹ub>a› by blast
  qed
  show "(poly p) sgnx_able (at_left a)"
  proof (cases "p=0")
    case True
    then show ?thesis unfolding sgnx_able_def has_sgnx_def eventually_at_right
      using linordered_field_no_ub by force
  next
    case False
    obtain lb where "lb<a" and ub:"∀z. lb≤z∧z<a⟶poly p z≠0" 
      using last_non_root_interval[OF False] by auto 
    have "∀z. lb≤z∧z<a⟶sgn(poly p z) = sgn (poly p lb)"
    proof (rule ccontr)
      assume "¬ (∀z. lb≤z∧z<a ⟶ sgn (poly p z) = sgn (poly p lb))"
      then obtain z where "lb≤z" "z<a" "sgn(poly p z) ≠ sgn (poly p lb)" by auto
      moreover then have "poly p z≠0" "poly p lb≠0" "z≠lb" using ub ‹lb<a› by blast+
      ultimately have "(poly p z>0 ∧ poly p lb<0) ∨ (poly p z<0 ∧ poly p lb>0)"
        by (metis linorder_neqE_linordered_idom sgn_neg sgn_pos)
      then have "∃x>lb. x < z ∧ poly p x = 0" 
        using poly_IVT_neg[of lb z p] poly_IVT_pos[of lb z p] ‹lb≤z› ‹z≠lb› by argo  
      then show False using ub ‹z < a› by auto  
    qed
    then show ?thesis unfolding sgnx_able_def has_sgnx_def eventually_at_left
      apply (rule_tac exI[where x="sgn(poly p lb)"])
      apply (rule_tac exI[where x="lb"])
      using less_eq_real_def ‹lb<a› by blast
  qed
qed

lemma has_sgnx_identity[intro,sgnx_intros]:
  shows "x≥0 ⟹((λx. x) has_sgnx 1) (at_right x)" 
        "x≤0 ⟹ ((λx. x) has_sgnx -1) (at_left x)"  
proof -
  show "x≥0 ⟹ ((λx. x) has_sgnx 1) (at_right x)"
    unfolding has_sgnx_def eventually_at_right
    apply (intro exI[where x="x+1"])
    by auto
  show "x≤0 ⟹ ((λx. x) has_sgnx -1) (at_left x)"
    unfolding has_sgnx_def eventually_at_left
    apply (intro exI[where x="x-1"])
    by auto
qed
    
lemma has_sgnx_divide[sgnx_intros]:
  assumes "(f has_sgnx c1) F" "(g has_sgnx c2) F"
  shows "((λx. f x / g x) has_sgnx c1 / c2) F"
proof -
  have "∀F x in F. sgn (f x) = c1 ∧ sgn (g x) = c2" 
    using assms unfolding has_sgnx_def by (intro eventually_conj,auto)
  then have "∀F x in F. sgn (f x / g x) = c1 / c2" 
    apply (elim eventually_mono)
    by (simp add: sgn_mult sgn_divide)
  then show "((λx. f x / g x) has_sgnx c1 / c2) F" unfolding has_sgnx_def by auto
qed

lemma sgnx_able_divide[sgnx_intros]:
  assumes "f sgnx_able F" "g sgnx_able F"
  shows "(λx. f x / g x) sgnx_able F"  
using has_sgnx_divide by (meson assms(1) assms(2) sgnx_able_def)   

lemma sgnx_divide:
  assumes "F≠bot" "f sgnx_able F" "g sgnx_able F"
  shows "sgnx (λx. f x / g x) F =sgnx f F / sgnx g F"
proof -
  obtain c1 c2 where c1:"(f has_sgnx c1) F" and c2:"(g has_sgnx c2) F"
    using assms unfolding sgnx_able_def by auto
  have "sgnx f F=c1" "sgnx g F=c2" using c1 c2 ‹F≠bot› by auto
  moreover have "((λx. f x / g x) has_sgnx c1 / c2) F" 
    using has_sgnx_divide[OF c1 c2] .
  ultimately show ?thesis using assms(1) has_sgnx_imp_sgnx by blast
qed
  
lemma has_sgnx_times[sgnx_intros]:
  assumes "(f has_sgnx c1) F" "(g has_sgnx c2) F"
  shows "((λx. f x* g x) has_sgnx c1 * c2) F"
proof -
  have "∀F x in F. sgn (f x) = c1 ∧ sgn (g x) = c2" 
    using assms unfolding has_sgnx_def by (intro eventually_conj,auto)
  then have "∀F x in F. sgn (f x * g x) = c1 * c2" 
    apply (elim eventually_mono)
    by (simp add: sgn_mult)
  then show "((λx. f x* g x) has_sgnx c1 * c2) F" unfolding has_sgnx_def by auto
qed

lemma sgnx_able_times[sgnx_intros]:
  assumes "f sgnx_able F" "g sgnx_able F"
  shows "(λx. f x * g x) sgnx_able F"  
using has_sgnx_times by (meson assms(1) assms(2) sgnx_able_def)   

lemma sgnx_times:
  assumes "F≠bot" "f sgnx_able F" "g sgnx_able F"
  shows "sgnx (λx. f x * g x) F =sgnx f F * sgnx g F"
proof -
  obtain c1 c2 where c1:"(f has_sgnx c1) F" and c2:"(g has_sgnx c2) F"
    using assms unfolding sgnx_able_def by auto
  have "sgnx f F=c1" "sgnx g F=c2" using c1 c2 ‹F≠bot› by auto
  moreover have "((λx. f x* g x) has_sgnx c1 * c2) F" 
    using has_sgnx_times[OF c1 c2] .
  ultimately show ?thesis using assms(1) has_sgnx_imp_sgnx by blast
qed

lemma tendsto_nonzero_has_sgnx:
  assumes "(f ⤏ c) F" "c≠0"
  shows "(f has_sgnx sgn c) F"
proof (cases rule:linorder_cases[of c 0])
  case less
  then have "∀F x in F. f x<0"
    using order_topology_class.order_tendstoD[OF assms(1),of 0] by auto
  then show ?thesis 
    unfolding has_sgnx_def 
    apply (elim eventually_mono)
    using less by auto
next
  case equal
  then show ?thesis using ‹c≠0› by auto
next
  case greater
  then have "∀F x in F. f x>0"
    using order_topology_class.order_tendstoD[OF assms(1),of 0] by auto
  then show ?thesis 
    unfolding has_sgnx_def 
    apply (elim eventually_mono)
    using greater by auto
qed

lemma tendsto_nonzero_sgnx:
  assumes "(f ⤏ c) F" "F≠bot" "c≠0"
  shows "sgnx f F = sgn c"
  using tendsto_nonzero_has_sgnx
by (simp add: assms has_sgnx_imp_sgnx)


lemma filterlim_divide_at_bot_at_top_iff:
  assumes "(f ⤏ c) F" "c≠0" 
  shows 
    "(LIM x F. f x / g x :> at_bot) ⟷ (g ⤏ 0) F 
      ∧ ((λx. g x) has_sgnx - sgn c) F"
    "(LIM x F. f x / g x :> at_top) ⟷ (g ⤏ 0) F 
      ∧ ((λx. g x) has_sgnx sgn c) F"
proof -
  show "(LIM x F. f x / g x :> at_bot) ⟷ ((g ⤏ 0) F )  
    ∧ ((λx. g x) has_sgnx - sgn c) F"
  proof 
    assume asm:"LIM x F. f x / g x :> at_bot"
    then have "filterlim g (at 0) F" 
      using filterlim_at_infinity_divide_iff[OF assms(1,2),of g] 
      at_bot_le_at_infinity filterlim_mono by blast
    then have "(g ⤏ 0) F" using filterlim_at by blast
    moreover have "(g has_sgnx - sgn c) F"
    proof -
      have "((λx. sgn c * inverse (f x)) ⤏ sgn c * inverse c) F"
        using assms(1,2) by (auto intro:tendsto_intros)
      then have "LIM x F. sgn c * inverse (f x) * (f x / g x) :> at_bot"
        apply (elim filterlim_tendsto_pos_mult_at_bot[OF _ _ asm])
        using ‹c≠0› sgn_real_def by auto
      then have "LIM x F. sgn c / g x :> at_bot"
        apply (elim filterlim_mono_eventually)
        using eventually_times_inverse_1[OF assms] by (auto elim:eventually_mono)
      then have "∀F x in F. sgn c / g x < 0" 
        using filterlim_at_bot_dense[of "λx. sgn c/g x" F] by auto
      then show ?thesis unfolding has_sgnx_def
        apply (elim eventually_mono)
        by (metis add.inverse_inverse divide_less_0_iff sgn_neg sgn_pos sgn_sgn)
    qed  
    ultimately show "(g ⤏ 0) F ∧ (g has_sgnx - sgn c) F" by auto
  next
    assume "(g ⤏ 0) F ∧ (g has_sgnx - sgn c) F"
    then have asm:"(g ⤏ 0) F" "(g has_sgnx - sgn c) F" by auto
    have "LIM x F. inverse (g x * sgn c) :> at_bot"
    proof (rule filterlim_inverse_at_bot)
      show "((λx. g x * sgn c) ⤏ 0) F"  
        apply (rule tendsto_mult_left_zero)
        using asm(1) by blast
    next
      show "∀F x in F. g x * sgn c < 0" using asm(2) unfolding has_sgnx_def
        apply (elim eventually_mono)
        by (metis add.inverse_inverse assms(2) linorder_neqE_linordered_idom mult_less_0_iff 
            neg_0_less_iff_less sgn_greater sgn_zero_iff)
    qed
    moreover have "((λx. f x * sgn c) ⤏ c * sgn c) F"
      using ‹(f ⤏ c) F› ‹c≠0›
      apply (intro tendsto_intros)
      by (auto simp add:sgn_zero_iff)
    moreover have "c * sgn c >0" using ‹c≠0› by (simp add: sgn_real_def)    
    ultimately have "LIM x F. (f x * sgn c) *inverse (g x * sgn c) :> at_bot"
      using filterlim_tendsto_pos_mult_at_bot by blast
    then show "LIM x F. f x / g x :> at_bot" 
      using ‹c≠0› by (auto simp add:field_simps sgn_zero_iff)
  qed
  show "(LIM x F. f x / g x :> at_top) ⟷ ((g ⤏ 0) F )  
    ∧ ((λx. g x) has_sgnx sgn c) F"
  proof 
    assume asm:"LIM x F. f x / g x :> at_top"
    then have "filterlim g (at 0) F" 
      using filterlim_at_infinity_divide_iff[OF assms(1,2),of g] 
      at_top_le_at_infinity filterlim_mono by blast
    then have "(g ⤏ 0) F" using filterlim_at by blast
    moreover have "(g has_sgnx sgn c) F"
    proof -
      have "((λx. sgn c * inverse (f x)) ⤏ sgn c * inverse c) F"
        using assms(1,2) by (auto intro:tendsto_intros)
      then have "LIM x F. sgn c * inverse (f x) * (f x / g x) :> at_top"
        apply (elim filterlim_tendsto_pos_mult_at_top[OF _ _ asm])
        using ‹c≠0› sgn_real_def by auto
      then have "LIM x F. sgn c / g x :> at_top"
        apply (elim filterlim_mono_eventually)
        using eventually_times_inverse_1[OF assms] by (auto elim:eventually_mono)
      then have "∀F x in F. sgn c / g x > 0" 
        using filterlim_at_top_dense[of "λx. sgn c/g x" F] by auto
      then show ?thesis unfolding has_sgnx_def
        apply (elim eventually_mono)
        by (metis sgn_greater sgn_less sgn_neg sgn_pos zero_less_divide_iff)
    qed  
    ultimately show "(g ⤏ 0) F ∧ (g has_sgnx sgn c) F" by auto
  next
    assume "(g ⤏ 0) F ∧ (g has_sgnx sgn c) F"
    then have asm:"(g ⤏ 0) F" "(g has_sgnx sgn c) F" by auto
    have "LIM x F. inverse (g x * sgn c) :> at_top"
    proof (rule filterlim_inverse_at_top)
      show "((λx. g x * sgn c) ⤏ 0) F"  
        apply (rule tendsto_mult_left_zero)
        using asm(1) by blast
    next
      show "∀F x in F. g x * sgn c > 0" using asm(2) unfolding has_sgnx_def
        apply (elim eventually_mono)
        by (metis assms(2) sgn_1_neg sgn_greater sgn_if zero_less_mult_iff)
    qed
    moreover have "((λx. f x * sgn c) ⤏ c * sgn c) F"
      using ‹(f ⤏ c) F› ‹c≠0›
      apply (intro tendsto_intros)
      by (auto simp add:sgn_zero_iff)
    moreover have "c * sgn c >0" using ‹c≠0› by (simp add: sgn_real_def)    
    ultimately have "LIM x F. (f x * sgn c) *inverse (g x * sgn c) :> at_top"
      using filterlim_tendsto_pos_mult_at_top by blast
    then show "LIM x F. f x / g x :> at_top" 
      using ‹c≠0› by (auto simp add:field_simps sgn_zero_iff)
  qed    
qed 


lemma poly_sgnx_left_right:
  fixes c a::real and p::"real poly"
  assumes "p≠0"
  shows "sgnx (poly p) (at_left a) = (if even (order a p) 
            then sgnx (poly p) (at_right a)
            else -sgnx (poly p) (at_right a))"
  using assms
proof (induction "degree p" arbitrary: p rule: less_induct)
  case less
  have ?case when "poly p a≠0" 
  proof -
    have "sgnx (poly p) (at_left a) = sgn (poly p a)" 
      by (simp add: has_sgnx_imp_sgnx tendsto_nonzero_has_sgnx that)
    moreover have "sgnx (poly p) (at_right a) = sgn (poly p a)"
      by (simp add: has_sgnx_imp_sgnx tendsto_nonzero_has_sgnx that)
    moreover have "order a p = 0" using that by (simp add: order_0I)
    ultimately show ?thesis by auto
  qed
  moreover have ?case when "poly p a=0"
  proof -
    obtain q where pq:"p= [:-a,1:] * q" 
      using ‹poly p a=0› by (meson dvdE poly_eq_0_iff_dvd)
    then have "q≠0" using ‹p≠0› by auto
    then have "degree q < degree p" unfolding pq by (subst degree_mult_eq,auto)
    have "sgnx (poly p) (at_left a) = - sgnx (poly q) (at_left a)" 
    proof -
      have "sgnx (λx. poly p x) (at_left a) 
          = sgnx (poly q) (at_left a) * sgnx (poly [:-a,1:]) (at_left a)"
        unfolding pq
        apply (subst poly_mult)
        apply (subst sgnx_times)
        by auto
      moreover have "sgnx (λx. poly [:-a,1:] x) (at_left a) = -1"
        apply (intro has_sgnx_imp_sgnx)
        unfolding has_sgnx_def eventually_at_left
        by (auto simp add: linordered_field_no_lb)
      ultimately show ?thesis by auto
    qed
    moreover have "sgnx (poly p) (at_right a) = sgnx (poly q) (at_right a)" 
    proof -
      have "sgnx (λx. poly p x) (at_right a) 
          = sgnx (poly q) (at_right a) * sgnx (poly [:-a,1:]) (at_right a)"
        unfolding pq
        apply (subst poly_mult)
        apply (subst sgnx_times)
        by auto
      moreover have "sgnx (λx. poly [:-a,1:] x) (at_right a) = 1"
        apply (intro has_sgnx_imp_sgnx)
        unfolding has_sgnx_def eventually_at_right
        by (auto simp add: linordered_field_no_ub)
      ultimately show ?thesis by auto
    qed
    moreover have "even (order a p) ⟷ odd (order a q)"
      unfolding pq 
      apply (subst order_mult[OF ‹p ≠ 0›[unfolded pq]])
      using  ‹q≠0› by (auto simp add:order_power_n_n[of _ 1, simplified])
    moreover note less.hyps[OF ‹degree q < degree p› ‹q≠0›]
    ultimately show ?thesis by auto
  qed
  ultimately show ?case by blast
qed

lemma poly_has_sgnx_left_right:
  fixes c a::real and p::"real poly"
  assumes "p≠0"
  shows "(poly p has_sgnx c) (at_left a) ⟷ (if even (order a p) 
            then (poly p has_sgnx c) (at_right a)
            else (poly p has_sgnx -c) (at_right a))"
using poly_sgnx_left_right 
by (metis (no_types, hide_lams) add.inverse_inverse assms has_sgnx_unique 
     sgnx_able_poly sgnx_able_sgnx trivial_limit_at_left_real trivial_limit_at_right_real)    
    
    
lemma sign_r_pos_sgnx_iff:
  "sign_r_pos p a ⟷ sgnx (poly p) (at_right a) > 0"
proof 
  assume asm:"0 < sgnx (poly p) (at_right a)"
  obtain c where c_def:"(poly p has_sgnx c) (at_right a)"
    using sgnx_able_poly(1) sgnx_able_sgnx by blast
  then have "c>0" using asm 
    using has_sgnx_imp_sgnx trivial_limit_at_right_real by blast
  then show "sign_r_pos p a" using c_def unfolding sign_r_pos_def has_sgnx_def
    apply (elim eventually_mono)
    by force
next
  assume asm:"sign_r_pos p a"
  define c where "c = sgnx (poly p) (at_right a)"
  then have "(poly p has_sgnx c) (at_right a)" 
    by (simp add: sgnx_able_sgnx)
  then have "(∀F x in (at_right a). poly p x>0 ∧ sgn (poly p x) = c)"
    using asm unfolding has_sgnx_def sign_r_pos_def
    by (simp add:eventually_conj_iff)
  then have "∀F x in (at_right a). c > 0"
    apply (elim eventually_mono)
    by fastforce
  then show "c>0" by auto
qed

lemma sgnx_values:
  assumes "f sgnx_able F" "F ≠ bot"
  shows "sgnx f F = -1 ∨ sgnx f F = 0 ∨ sgnx f F = 1"
proof -
  obtain c where c_def:"(f has_sgnx c) F" 
    using assms(1) unfolding sgnx_able_def by auto
  then obtain x where "sgn(f x) = c" 
    unfolding has_sgnx_def using assms(2) eventually_happens 
    by blast
  then have "c=-1 ∨ c=0 ∨ c=1" using sgn_if by metis
  moreover have "sgnx f F = c" using c_def by (simp add: assms(2) has_sgnx_imp_sgnx)
  ultimately show ?thesis by auto
qed
  
lemma has_sgnx_poly_at_top:
    "(poly p has_sgnx  sgn_pos_inf p) at_top"
  using has_sgnx_def poly_sgn_eventually_at_top by blast

lemma has_sgnx_poly_at_bot:
    "(poly p has_sgnx  sgn_neg_inf p) at_bot"
  using has_sgnx_def poly_sgn_eventually_at_bot by blast
    
lemma sgnx_poly_at_top:
  "sgnx (poly p) at_top = sgn_pos_inf p"
by (simp add: has_sgnx_def has_sgnx_imp_sgnx poly_sgn_eventually_at_top)
    
lemma sgnx_poly_at_bot:
  "sgnx (poly p) at_bot = sgn_neg_inf p"
by (simp add: has_sgnx_def has_sgnx_imp_sgnx poly_sgn_eventually_at_bot)  
  
lemma poly_has_sgnx_values:
  assumes "p≠0"
  shows 
    "(poly p has_sgnx 1) (at_left a) ∨ (poly p has_sgnx - 1) (at_left a)"
    "(poly p has_sgnx 1) (at_right a) ∨ (poly p has_sgnx - 1) (at_right a)"
    "(poly p has_sgnx 1) at_top ∨ (poly p has_sgnx - 1) at_top"
    "(poly p has_sgnx 1) at_bot ∨ (poly p has_sgnx - 1) at_bot"
proof -
  have "sgn_pos_inf p = 1 ∨ sgn_pos_inf p = -1"
    unfolding sgn_pos_inf_def by (simp add: assms sgn_if)
  then show "(poly p has_sgnx 1) at_top ∨ (poly p has_sgnx - 1) at_top"
    using has_sgnx_poly_at_top by metis
next
  have "sgn_neg_inf p = 1 ∨ sgn_neg_inf p = -1"
    unfolding sgn_neg_inf_def by (simp add: assms sgn_if)
  then show "(poly p has_sgnx 1) at_bot ∨ (poly p has_sgnx - 1) at_bot"
    using has_sgnx_poly_at_bot by metis
next
  obtain c where c_def:"(poly p has_sgnx c) (at_left a)" 
    using sgnx_able_poly(2) sgnx_able_sgnx by blast
  then have "sgnx (poly p) (at_left a) = c" using assms by auto
  then have "c=-1 ∨ c=0 ∨ c=1"
    using sgnx_values sgnx_able_poly(2) trivial_limit_at_left_real by blast
  moreover have False when "c=0" 
  proof -
    have "(poly p has_sgnx 0) (at_left a)" using c_def that by auto
    then obtain lb where "lb<a" "∀y. (lb<y ∧ y < a) ⟶ poly p y = 0"
      unfolding has_sgnx_def eventually_at_left sgn_if
      by (metis one_neq_zero zero_neq_neg_one)
    then have "{lb<..<a} ⊆ proots p" unfolding proots_within_def by auto
    then have "infinite (proots p)"
      apply (elim infinite_super)
      using ‹lb<a› by auto
    moreover have "finite (proots p)" using finite_proots[OF ‹p≠0›] by auto
    ultimately show False by auto
  qed
  ultimately have "c=-1 ∨ c=1" by auto
  then show "(poly p has_sgnx 1) (at_left a) ∨ (poly p has_sgnx - 1) (at_left a)"
    using c_def by auto
next
  obtain c where c_def:"(poly p has_sgnx c) (at_right a)" 
    using sgnx_able_poly(1) sgnx_able_sgnx by blast
  then have "sgnx (poly p) (at_right a) = c" using assms by auto
  then have "c=-1 ∨ c=0 ∨ c=1"
    using sgnx_values sgnx_able_poly(1) trivial_limit_at_right_real by blast
  moreover have False when "c=0" 
  proof -
    have "(poly p has_sgnx 0) (at_right a)" using c_def that by auto
    then obtain ub where "ub>a" "∀y. (a<y ∧ y < ub) ⟶ poly p y = 0"
      unfolding has_sgnx_def eventually_at_right sgn_if
      by (metis one_neq_zero zero_neq_neg_one)
    then have "{a<..<ub} ⊆ proots p" unfolding proots_within_def by auto
    then have "infinite (proots p)"
      apply (elim infinite_super)
      using ‹ub>a› by auto
    moreover have "finite (proots p)" using finite_proots[OF ‹p≠0›] by auto
    ultimately show False by auto
  qed
  ultimately have "c=-1 ∨ c=1" by auto
  then show "(poly p has_sgnx 1) (at_right a) ∨ (poly p has_sgnx - 1) (at_right a)"
    using c_def by auto
qed

lemma poly_sgnx_values:
  assumes "p≠0"
  shows "sgnx (poly p) (at_left a) = 1 ∨ sgnx (poly p) (at_left a) = -1"
        "sgnx (poly p) (at_right a) = 1 ∨ sgnx (poly p) (at_right a) = -1" 
  using poly_has_sgnx_values[OF ‹p≠0›] has_sgnx_imp_sgnx trivial_limit_at_left_real 
    trivial_limit_at_right_real by blast+
 
lemma has_sgnx_inverse: "(f has_sgnx c) F ⟷ ((inverse o f) has_sgnx (inverse c)) F"
  unfolding has_sgnx_def comp_def
  apply (rule eventually_subst)  
  apply (rule always_eventually)
  by (metis inverse_inverse_eq sgn_inverse)


lemma has_sgnx_derivative_at_left:
  assumes g_deriv:"(g has_field_derivative c) (at x)" and "g x=0" and "c≠0" 
  shows "(g has_sgnx - sgn c) (at_left x)" 
proof -
  have "(g has_sgnx -1) (at_left x)" when "c>0"
  proof -
    obtain d1 where "d1>0" and d1_def:"∀h>0. h < d1 ⟶ g (x - h) < g x"
      using DERIV_pos_inc_left[OF g_deriv ‹c>0›] ‹g x=0› by auto
    have "(g has_sgnx -1) (at_left x)" 
      unfolding has_sgnx_def eventually_at_left
      apply (intro exI[where x="x-d1"])
      using ‹d1>0› d1_def 
      by (metis (no_types, hide_lams) add.commute add_uminus_conv_diff assms(2) diff_add_cancel 
          diff_strict_left_mono diff_zero minus_diff_eq sgn_neg)  
    thus ?thesis by auto 
  qed
  moreover have "(g has_sgnx 1) (at_left x)" when "c<0"
  proof -
    obtain d1 where "d1>0" and d1_def:"∀h>0. h < d1 ⟶ g (x - h) > g x"
        using DERIV_neg_dec_left[OF g_deriv ‹c<0›] ‹g x=0› by auto
    have "(g has_sgnx 1) (at_left x)" 
        unfolding has_sgnx_def eventually_at_left
        apply (intro exI[where x="x-d1"])
        using ‹d1>0› d1_def 
        by (metis (no_types, hide_lams) add.commute add_uminus_conv_diff assms(2) diff_add_cancel
            diff_zero less_diff_eq minus_diff_eq sgn_pos)
    thus ?thesis using ‹c<0›  by auto
  qed
  ultimately show ?thesis using ‹c≠0› using sgn_real_def by auto
qed

lemma has_sgnx_derivative_at_right:
  assumes g_deriv:"(g has_field_derivative c) (at x)" and "g x=0" and "c≠0"
  shows "(g has_sgnx sgn c) (at_right x)"  
proof -
  have "(g has_sgnx 1) (at_right x)" when "c>0"
  proof -
    obtain d2 where "d2>0" and d2_def:"∀h>0. h < d2 ⟶ g x < g (x + h)"
        using DERIV_pos_inc_right[OF g_deriv ‹c>0›] ‹g x=0› by auto 
    have "(g has_sgnx 1) (at_right x)" 
      unfolding has_sgnx_def eventually_at_right
      apply (intro exI[where x="x+d2"])
      using ‹d2>0› d2_def 
      by (metis add.commute assms(2) diff_add_cancel diff_less_eq less_add_same_cancel1 sgn_pos)
    thus ?thesis using ‹c>0› by auto
  qed
  moreover have "(g has_sgnx -1) (at_right x)" when "c<0"
  proof -
    obtain d2 where "d2>0" and d2_def:"∀h>0. h < d2 ⟶ g x > g (x + h)"
      using DERIV_neg_dec_right[OF g_deriv ‹c<0›] ‹g x=0› by auto 
    have "(g has_sgnx -1) (at_right x)" 
      unfolding has_sgnx_def eventually_at_right
      apply (intro exI[where x="x+d2"])
      using ‹d2>0› d2_def 
      by (metis (no_types, hide_lams) add.commute add.right_inverse add_uminus_conv_diff assms(2) 
          diff_add_cancel diff_less_eq sgn_neg)
    thus ?thesis using ‹c<0› by auto
  qed
  ultimately show ?thesis using ‹c≠0› using sgn_real_def by auto
qed  

lemma has_sgnx_split:
  "(f has_sgnx c) (at x) ⟷ (f has_sgnx c) (at_left x) ∧ (f has_sgnx c) (at_right x)"
unfolding has_sgnx_def using eventually_at_split by auto    
        
lemma sgnx_at_top_IVT:
  assumes "sgnx (poly p) (at_right a) ≠ sgnx (poly p) at_top"
  shows "∃x>a. poly p x=0"
proof (cases "p=0")
  case True
  then show ?thesis using gt_ex[of a] by simp
next
  case False
  from poly_has_sgnx_values[OF this] 
  have "(poly p has_sgnx 1) (at_right a) ∨ (poly p has_sgnx - 1) (at_right a)"
    "(poly p has_sgnx 1) at_top ∨ (poly p has_sgnx - 1) at_top"
    by auto
  moreover have ?thesis when has_r:"(poly p has_sgnx 1) (at_right a)" 
      and has_top:"(poly p has_sgnx -1) at_top"
  proof -
    obtain b where "b>a" "poly p b>0"
    proof -
      obtain a' where "a'>a" and a'_def:"∀y>a. y < a' ⟶ sgn (poly p y) = 1"
        using has_r[unfolded has_sgnx_def eventually_at_right] by auto
      define b where "b=(a+a')/2"
      have "a<b" "b<a'" unfolding b_def using ‹a'>a› by auto
      moreover have "poly p b>0"
        using a'_def[rule_format,OF ‹b>a› ‹b<a'›] unfolding sgn_if by argo
      ultimately show ?thesis using that by auto
    qed
    moreover obtain c where "c>b" "poly p c<0"
    proof -
      obtain b' where b'_def:"∀n≥b'. sgn (poly p n) = - 1"
        using has_top[unfolded has_sgnx_def eventually_at_top_linorder] by auto
      define c where "c=1+max b b'"
      have "c>b" "c≥b'" unfolding c_def using ‹b>a› by auto
      moreover have "poly p c<0"
        using b'_def[rule_format,OF ‹b'≤c›] unfolding sgn_if by argo
      ultimately show ?thesis using that by auto
    qed
    ultimately show ?thesis using poly_IVT_neg[of b c p] not_less by fastforce
  qed
  moreover have ?thesis when has_r:"(poly p has_sgnx -1) (at_right a)" 
      and has_top:"(poly p has_sgnx 1) at_top"
  proof -
    obtain b where "b>a" "poly p b<0"
    proof -
      obtain a' where "a'>a" and a'_def:"∀y>a. y < a' ⟶ sgn (poly p y) = -1"
        using has_r[unfolded has_sgnx_def eventually_at_right] by auto
      define b where "b=(a+a')/2"
      have "a<b" "b<a'" unfolding b_def using ‹a'>a› by auto
      moreover have "poly p b<0"
        using a'_def[rule_format,OF ‹b>a› ‹b<a'›] unfolding sgn_if by argo
      ultimately show ?thesis using that by auto
    qed
    moreover obtain c where "c>b" "poly p c>0"
    proof -
      obtain b' where b'_def:"∀n≥b'. sgn (poly p n) = 1"
        using has_top[unfolded has_sgnx_def eventually_at_top_linorder] by auto
      define c where "c=1+max b b'"
      have "c>b" "c≥b'" unfolding c_def using ‹b>a› by auto
      moreover have "poly p c>0"
        using b'_def[rule_format,OF ‹b'≤c›] unfolding sgn_if by argo
      ultimately show ?thesis using that by auto
    qed
    ultimately show ?thesis using poly_IVT_pos[of b c p] not_less by fastforce
  qed
  moreover have ?thesis when 
    "(poly p has_sgnx 1) (at_right a) ∧ (poly p has_sgnx 1) at_top
     ∨ (poly p has_sgnx - 1) (at_right a) ∧ (poly p has_sgnx -1) at_top" 
  proof -
    have "sgnx (poly p) (at_right a) = sgnx (poly p) at_top"
      using that has_sgnx_imp_sgnx by auto
    then have False using assms by simp
    then show ?thesis by auto
  qed
  ultimately show ?thesis by blast
qed
  
lemma sgnx_at_left_at_right_IVT:
  assumes "sgnx (poly p) (at_right a) ≠ sgnx (poly p) (at_left b)" "a<b"
  shows "∃x. a<x ∧ x<b ∧ poly p x=0"
proof (cases "p=0")
  case True
  then show ?thesis using ‹a<b› by (auto intro:exI[where x="(a+b)/2"])
next
  case False
  from poly_has_sgnx_values[OF this]
  have "(poly p has_sgnx 1) (at_right a) ∨ (poly p has_sgnx - 1) (at_right a)"
    "(poly p has_sgnx 1) (at_left b) ∨ (poly p has_sgnx - 1) (at_left b)"
    by auto
  moreover have ?thesis when has_r:"(poly p has_sgnx 1) (at_right a)" 
      and has_l:"(poly p has_sgnx -1) (at_left b)"
  proof -
    obtain c where "a<c" "c<b" "poly p c>0"
    proof -
      obtain a' where "a'>a" and a'_def:"∀y>a. y < a' ⟶ sgn (poly p y) = 1"
        using has_r[unfolded has_sgnx_def eventually_at_right] by auto
      define c where "c=(a+min a' b)/2"
      have "a<c" "c<a'" "c<b" unfolding c_def using ‹a'>a› ‹b>a› by auto
      moreover have "poly p c>0"
        using a'_def[rule_format,OF ‹c>a› ‹c<a'›] unfolding sgn_if by argo
      ultimately show ?thesis using that by auto
    qed
    moreover obtain d where "c<d""d<b" "poly p d<0"
    proof -
      obtain b' where "b'<b" and b'_def:"∀y>b'. y < b ⟶ sgn (poly p y) = - 1"
        using has_l[unfolded has_sgnx_def eventually_at_left] by auto
      define d where "d=(b+max b' c)/2"
      have "b'<d" "d<b" "d>c" 
        unfolding d_def using ‹b>b'› ‹b>c› by auto
      moreover have "poly p d<0"
        using b'_def[rule_format, OF ‹b'<d› ‹d<b›] unfolding sgn_if by argo
      ultimately show ?thesis using that by auto
    qed
    ultimately obtain x where "c<x" "x<d" "poly p x=0"
      using poly_IVT_neg[of c d p] by auto
    then show ?thesis using ‹c>a› ‹d<b› by (auto intro: exI[where x=x])
  qed
  moreover have ?thesis when has_r:"(poly p has_sgnx -1) (at_right a)" 
      and has_l:"(poly p has_sgnx 1) (at_left b)"
  proof -
    obtain c where "a<c" "c<b" "poly p c<0"
    proof -
      obtain a' where "a'>a" and a'_def:"∀y>a. y < a' ⟶ sgn (poly p y) = -1"
        using has_r[unfolded has_sgnx_def eventually_at_right] by auto
      define c where "c=(a+min a' b)/2"
      have "a<c" "c<a'" "c<b" unfolding c_def using ‹a'>a› ‹b>a› by auto
      moreover have "poly p c<0"
        using a'_def[rule_format,OF ‹c>a› ‹c<a'›] unfolding sgn_if by argo
      ultimately show ?thesis using that by auto
    qed
    moreover obtain d where "c<d""d<b" "poly p d>0"
    proof -
      obtain b' where "b'<b" and b'_def:"∀y>b'. y < b ⟶ sgn (poly p y) = 1"
        using has_l[unfolded has_sgnx_def eventually_at_left] by auto
      define d where "d=(b+max b' c)/2"
      have "b'<d" "d<b" "d>c" 
        unfolding d_def using ‹b>b'› ‹b>c› by auto
      moreover have "poly p d>0"
        using b'_def[rule_format, OF ‹b'<d› ‹d<b›] unfolding sgn_if by argo
      ultimately show ?thesis using that by auto
    qed
    ultimately obtain x where "c<x" "x<d" "poly p x=0"
      using poly_IVT_pos[of c d p] by auto
    then show ?thesis using ‹c>a› ‹d<b› by (auto intro: exI[where x=x])
  qed
  moreover have ?thesis when 
    "(poly p has_sgnx 1) (at_right a) ∧ (poly p has_sgnx 1) (at_left b)
     ∨ (poly p has_sgnx - 1) (at_right a) ∧ (poly p has_sgnx -1) (at_left b)" 
  proof -
    have "sgnx (poly p) (at_right a) = sgnx (poly p) (at_left b)"
      using that has_sgnx_imp_sgnx by auto
    then have False using assms by simp
    then show ?thesis by auto
  qed
  ultimately show ?thesis by blast
qed
   
lemma sgnx_at_bot_IVT:
  assumes "sgnx (poly p) (at_left a) ≠ sgnx (poly p) at_bot"
  shows "∃x<a. poly p x=0"
proof (cases "p=0")
  case True
  then show ?thesis using lt_ex[of a] by simp
next
  case False
  from poly_has_sgnx_values[OF this] 
  have "(poly p has_sgnx 1) (at_left a) ∨ (poly p has_sgnx - 1) (at_left a)"
    "(poly p has_sgnx 1) at_bot ∨ (poly p has_sgnx - 1) at_bot"
    by auto
  moreover have ?thesis when has_l:"(poly p has_sgnx 1) (at_left a)" 
      and has_bot:"(poly p has_sgnx -1) at_bot"
  proof -
    obtain b where "b<a" "poly p b>0"
    proof -
      obtain a' where "a'<a" and a'_def:"∀y>a'. y < a ⟶ sgn (poly p y) = 1"
        using has_l[unfolded has_sgnx_def eventually_at_left] by auto
      define b where "b=(a+a')/2"
      have "a>b" "b>a'" unfolding b_def using ‹a'<a› by auto
      moreover have "poly p b>0"
        using a'_def[rule_format,OF ‹b>a'› ‹b<a›] unfolding sgn_if by argo
      ultimately show ?thesis using that by auto
    qed
    moreover obtain c where "c<b" "poly p c<0"
    proof -
      obtain b' where b'_def:"∀n≤b'. sgn (poly p n) = - 1"
        using has_bot[unfolded has_sgnx_def eventually_at_bot_linorder] by auto
      define c where "c=min b b'- 1"
      have "c<b" "c≤b'" unfolding c_def using ‹b<a› by auto
      moreover have "poly p c<0"
        using b'_def[rule_format,OF ‹b'≥c›] unfolding sgn_if by argo
      ultimately show ?thesis using that by auto
    qed
    ultimately show ?thesis using poly_IVT_pos[of c b p] using not_less by fastforce
  qed
  moreover have ?thesis when has_l:"(poly p has_sgnx -1) (at_left a)" 
      and has_bot:"(poly p has_sgnx 1) at_bot"
  proof -
    obtain b where "b<a" "poly p b<0"
    proof -
      obtain a' where "a'<a" and a'_def:"∀y>a'. y < a ⟶ sgn (poly p y) = -1"
        using has_l[unfolded has_sgnx_def eventually_at_left] by auto
      define b where "b=(a+a')/2"
      have "a>b" "b>a'" unfolding b_def using ‹a'<a› by auto
      moreover have "poly p b<0"
        using a'_def[rule_format,OF ‹b>a'› ‹b<a›] unfolding sgn_if by argo
      ultimately show ?thesis using that by auto
    qed
    moreover obtain c where "c<b" "poly p c>0"
    proof -
      obtain b' where b'_def:"∀n≤b'. sgn (poly p n) = 1"
        using has_bot[unfolded has_sgnx_def eventually_at_bot_linorder] by auto
      define c where "c=min b b'- 1"
      have "c<b" "c≤b'" unfolding c_def using ‹b<a› by auto
      moreover have "poly p c>0"
        using b'_def[rule_format,OF ‹b'≥c›] unfolding sgn_if by argo
      ultimately show ?thesis using that by auto
    qed
    ultimately show ?thesis using poly_IVT_neg[of c b p] using not_less by fastforce
  qed
  moreover have ?thesis when 
    "(poly p has_sgnx 1) (at_left a) ∧ (poly p has_sgnx 1) at_bot
     ∨ (poly p has_sgnx - 1) (at_left a) ∧ (poly p has_sgnx -1) at_bot" 
  proof -
    have "sgnx (poly p) (at_left a) = sgnx (poly p) at_bot"
      using that has_sgnx_imp_sgnx by auto
    then have False using assms by simp
    then show ?thesis by auto
  qed
  ultimately show ?thesis by blast
qed    

lemma sgnx_poly_nz:
  assumes "poly p x≠0"
  shows "sgnx (poly p) (at_left x) = sgn (poly p x)"
        "sgnx (poly p) (at_right x) = sgn (poly p x)"
proof -
  have "(poly p has_sgnx sgn(poly p x)) (at x)"
    apply (rule tendsto_nonzero_has_sgnx)
    using assms by auto
  then show "sgnx (poly p) (at_left x) = sgn (poly p x)"
        "sgnx (poly p) (at_right x) = sgn (poly p x)"
    unfolding has_sgnx_split by auto
qed
  
subsection ‹Finite predicate segments over an interval›

inductive finite_Psegments::"(real ⇒ bool) ⇒ real ⇒ real ⇒ bool" for P where
  emptyI: "a≥b ⟹ finite_Psegments P a b"|
  insertI_1: "⟦s∈{a..<b};s=a∨P s;∀t∈{s<..<b}. P t; finite_Psegments P a s⟧ 
        ⟹ finite_Psegments P a b"|
  insertI_2: "⟦s∈{a..<b};s=a∨P s;(∀t∈{s<..<b}. ¬P t);finite_Psegments P a s⟧ 
        ⟹ finite_Psegments P a b" 

lemma finite_Psegments_pos_linear:
  assumes "finite_Psegments P (b*lb+c) (b*ub+c) " and "b>0"
  shows "finite_Psegments (P o (λt. b*t+c)) lb ub" 
proof -    
  have [simp]:"b≠0" using ‹b>0› by auto
  show ?thesis 
  proof (rule finite_Psegments.induct[OF assms(1),
        of "λlb' ub'. finite_Psegments (P o (λt. b*t+c)) ((lb'-c)/b) ((ub'-c)/b)",simplified])
    (*really weird application of the induction rule, is there an alternative?*)
    fix lb ub f assume "(lb::real)≤ub"  
    then have "(lb - c) / b ≤ (ub - c) / b" 
      using ‹b>0› by (auto simp add:field_simps)
    then show "finite_Psegments (f ∘ (λt. b * t + c)) ((ub - c) / b) ((lb - c) / b)"
      by (rule finite_Psegments.emptyI)
  next
    fix s lb ub P
    assume asm: "lb ≤ s ∧ s < ub" 
       "∀t∈{s<..<ub}. P t" 
       "finite_Psegments (P ∘ (λt. b * t + c)) ((lb - c) / b) ((s - c) / b)"
       "s = lb ∨ P s"
    show "finite_Psegments (P ∘ (λt. b * t + c)) ((lb - c) / b) ((ub - c) / b)"
      apply (rule finite_Psegments.insertI_1[of "(s-c)/b"])
      using asm ‹b>0›  by (auto simp add:field_simps)
  next
    fix s lb ub P
    assume asm: "lb ≤ s ∧ s < ub" 
       "∀t∈{s<..<ub}. ¬ P t" 
       "finite_Psegments (P ∘ (λt. b * t + c)) ((lb - c) / b) ((s - c) / b)" 
       "s=lb ∨ P s"
    show "finite_Psegments (P ∘ (λt. b * t + c)) ((lb - c) / b) ((ub - c) / b)"
      apply (rule finite_Psegments.insertI_2[of "(s-c)/b"])
      using asm ‹b>0›  by (auto simp add:field_simps)
  qed
qed  

lemma finite_Psegments_congE:
  assumes "finite_Psegments Q lb ub" 
    "⋀t. ⟦lb<t;t<ub⟧ ⟹ Q t ⟷ P t "
  shows "finite_Psegments P lb ub" using assms
proof (induct rule:finite_Psegments.induct)
  case (emptyI a b)
  then show ?case using finite_Psegments.emptyI by auto
next
  case (insertI_1 s a b)
  show ?case 
  proof (rule finite_Psegments.insertI_1[of s])
    have "P s" when "s≠a"
    proof -
      have "s∈{a<..<b}" using ‹s ∈ {a..<b}› that by auto 
      then show ?thesis using insertI_1 by auto
    qed
    then show "s = a ∨ P s" by auto
  next
    show "s ∈ {a..<b}" " ∀t∈{s<..<b}. P t" "finite_Psegments P a s" using insertI_1 by auto
  qed  
next
  case (insertI_2 s a b)
  show ?case 
  proof (rule finite_Psegments.insertI_2[of s]) 
    have "P s" when "s≠a"
    proof -
      have "s∈{a<..<b}" using ‹s ∈ {a..<b}› that by auto 
      then show ?thesis using insertI_2 by auto
    qed
    then show "s = a ∨ P s" by auto
  next
    show "s ∈ {a..<b}" " ∀t∈{s<..<b}. ¬ P t" "finite_Psegments P a s" using insertI_2 by auto
  qed   
qed
  
lemma finite_Psegments_constI:
  assumes "⋀t. ⟦a<t;t<b⟧ ⟹ P t = c"
  shows "finite_Psegments P a b"
proof -
  have "finite_Psegments (λ_. c) a b"
  proof -
    have ?thesis when "a≥b"
      using that finite_Psegments.emptyI by auto
    moreover have ?thesis when "a<b" "c"
      apply (rule finite_Psegments.insertI_1[of a])
      using that by (auto intro: finite_Psegments.emptyI)
    moreover have ?thesis when "a<b" "¬c"
      apply (rule finite_Psegments.insertI_2[of a])
      using that by (auto intro: finite_Psegments.emptyI)
    ultimately show ?thesis by argo
  qed
  then show ?thesis
    apply (elim finite_Psegments_congE)
    using assms by auto
qed    

context 
begin  

private lemma finite_Psegments_less_eq1:
  assumes "finite_Psegments P a c" "b≤c"
  shows "finite_Psegments P a b" using assms
proof (induct arbitrary: b rule:finite_Psegments.induct)
  case (emptyI a c)
  then show ?case using finite_Psegments.emptyI by auto
next
  case (insertI_1 s a c)  
  have ?case when "b≤s" using insertI_1 that by auto
  moreover have ?case when "b>s" 
  proof -
    have "s ∈ {a..<b}" using that ‹s ∈ {a..<c}› ‹b ≤ c› by auto 
    moreover have "∀t∈{s<..<b}. P t" using ‹∀t∈{s<..<c}. P t› that ‹b ≤ c› by auto
    ultimately show ?case 
      using finite_Psegments.insertI_1[OF _ _ _ ‹finite_Psegments P a s›] ‹ s = a ∨ P s› by auto
  qed
  ultimately show ?case by fastforce
next
  case (insertI_2 s a c)
  have ?case when "b≤s" using insertI_2 that by auto
  moreover have ?case when "b>s" 
  proof -
    have "s ∈ {a..<b}" using that ‹s ∈ {a..<c}› ‹b ≤ c› by auto 
    moreover have "∀t∈{s<..<b}. ¬ P t" using ‹∀t∈{s<..<c}. ¬ P t› that ‹b ≤ c› by auto
    ultimately show ?case 
      using finite_Psegments.insertI_2[OF _ _ _ ‹finite_Psegments P a s›] ‹ s = a ∨ P s› by auto
  qed
  ultimately show ?case by fastforce
qed  
 
  
private lemma finite_Psegments_less_eq2:
  assumes "finite_Psegments P a c" "a≤b"
  shows "finite_Psegments P b c" using assms  
proof (induct arbitrary:  rule:finite_Psegments.induct)
  case (emptyI a c)
  then show ?case using finite_Psegments.emptyI by auto 
next
  case (insertI_1 s a c)
  have ?case when "s≤b"
  proof -
    have "∀t∈{b<..<c}. P t" using insertI_1 that by auto
    then show ?thesis by (simp add: finite_Psegments_constI)
  qed
  moreover have ?case when "s>b"
    apply (rule finite_Psegments.insertI_1[where s=s])
    using insertI_1 that by auto
  ultimately show ?case by linarith
next
  case (insertI_2 s a c)
  have ?case when "s≤b"
  proof -
    have "∀t∈{b<..<c}. ¬ P t" using insertI_2 that by auto
    then show ?thesis by (metis finite_Psegments_constI greaterThanLessThan_iff)
  qed
  moreover have ?case when "s>b"
    apply (rule finite_Psegments.insertI_2[where s=s])
    using insertI_2 that by auto
  ultimately show ?case by linarith
qed  


lemma finite_Psegments_included:
  assumes "finite_Psegments P a d" "a≤b" "c≤d"
  shows "finite_Psegments P b c"  
  using finite_Psegments_less_eq2 finite_Psegments_less_eq1 assms by blast      
end      

lemma finite_Psegments_combine:
  assumes "finite_Psegments P a b" "finite_Psegments P b c" "b∈{a..c}" "closed ({x. P x} ∩ {a..c})" 
  shows "finite_Psegments P a c"  using assms(2,1,3,4)
proof (induct rule:finite_Psegments.induct)
  case (emptyI b c)
  then show ?case using finite_Psegments_included by auto
next
  case (insertI_1 s b c)
  have "P s" 
  proof -
    have "s<c" using insertI_1 by auto
    define S where "S = {x. P x} ∩ {s..(s+c)/2}"
    have "closed S"
    proof -
      have "closed ({a. P a} ∩ {a..c})" using insertI_1(8) .
      moreover have "S = ({a. P a} ∩ {a..c}) ∩ {s..(s+c)/2}"
        using insertI_1(1,7) unfolding S_def by (auto simp add:field_simps)
      ultimately show ?thesis
        using closed_Int[of "{a. P a} ∩ {a..c}" "{s..(s+c)/2}"] by blast
    qed
    moreover have "∃y∈S. dist y s < e" when "e>0" for e 
    proof -
      define y where "y = min ((s+c)/2) (e/2+s)"
      have "y∈S"
      proof -
        have "y∈{s..(s+c)/2}" unfolding y_def
          using ‹e>0› ‹s<c› by (auto simp add:min_mult_distrib_left algebra_simps)
        moreover have "P y" 
          apply (rule insertI_1(3)[rule_format])
          unfolding y_def
          using ‹e>0› ‹s<c› 
          by (auto simp add:algebra_simps min_mult_distrib_left min_less_iff_disj)
        ultimately show ?thesis unfolding S_def by auto   
      qed
      moreover have "dist y s <e"
        unfolding y_def using ‹e>0› ‹s<c› 
        by (auto simp add:algebra_simps min_mult_distrib_left min_less_iff_disj dist_real_def)
      ultimately show ?thesis by auto
    qed
    ultimately have "s∈S" using closed_approachable by auto
    then show ?thesis unfolding S_def by auto
  qed
  show ?case 
  proof (rule finite_Psegments.insertI_1[of s])
    show " s ∈ {a..<c}" "s = a ∨ P s" "∀t∈{s<..<c}. P t"
      using insertI_1 ‹P s› by auto
  next
    have "closed ({a. P a} ∩ {a..s})" 
      using closed_Int[OF ‹closed ({a. P a} ∩ {a..c})›,of "{a..s}",simplified]
      apply (elim arg_elim[of closed])
      using ‹s ∈ {b..<c}› ‹b ∈ {a..c}› by auto
    then show "finite_Psegments P a s" using insertI_1 by auto
  qed
next
  case (insertI_2 s b c)
  have ?case when "P s"
  proof (rule finite_Psegments.insertI_2[of s])
    show "s ∈ {a..<c}" "s = a ∨ P s" "∀t∈{s<..<c}. ¬ P t" using that insertI_2 by auto
  next
    have "closed ({a. P a} ∩ {a..s})" 
      using closed_Int[OF ‹closed ({a. P a} ∩ {a..c})›,of "{a..s}",simplified]
      apply (elim arg_elim[of closed])
      using  ‹s ∈ {b..<c}› ‹b ∈ {a..c}› by auto
    then show "finite_Psegments P a s" using insertI_2 by auto
  qed  
  moreover have ?case when "¬ P s" "s=b" using ‹finite_Psegments P a b›  
  proof (cases rule:finite_Psegments.cases)
    case emptyI
    then show ?thesis using insertI_2 that 
      by (metis antisym_conv atLeastAtMost_iff finite_Psegments.insertI_2)
  next
    case (insertI_1 s0)
    have "P s" 
    proof -
      have "s0<s" using insertI_1 atLeastLessThan_iff that(2) by blast    
      define S where "S = {x. P x} ∩ {(s0+s)/2..s}"
      have "closed S"
        using closed_Int[OF ‹closed ({a. P a} ∩ {a..c})›,of "{(s0+s)/2..s}",simplified]  
        apply (elim arg_elim[of closed])
        unfolding S_def using ‹s0 ∈ {a..<b}› ‹ s ∈ {b..<c}› ‹b ∈ {a..c}› by auto    
      moreover have "∃y∈S. dist y s < e" when "e>0" for e 
      proof -
        define y where "y = max ((s+s0)/2) (s-e/2)"
        have "y∈S"
        proof -
          have "y∈{(s0+s)/2..s}" unfolding y_def
            using ‹e>0› ‹s0<s› by (auto simp add:field_simps min_mult_distrib_left)
          moreover have "P y" 
            apply (rule insertI_1(3)[rule_format])
            unfolding y_def
            using ‹e>0› ‹s0<s› ‹s=b›
            by (auto simp add:field_simps max_mult_distrib_left less_max_iff_disj)
          ultimately show ?thesis unfolding S_def by auto   
        qed
        moreover have "dist y s <e"
          unfolding y_def using ‹e>0› ‹s0<s› 
          by (auto simp add:algebra_simps max_mult_distrib_left less_max_iff_disj dist_real_def 
              max_add_distrib_right)
        ultimately show ?thesis by auto
      qed
      ultimately have "s∈S" using closed_approachable by auto
      then show ?thesis unfolding S_def by auto
    qed  
    then have False using ‹¬ P s› by auto
    then show ?thesis by simp
  next
    case (insertI_2 s0)
    have *: "∀t∈{s0<..<c}. ¬ P t" 
      using ‹ ∀t∈{s<..<c}. ¬ P t› that ‹∀t∈{s0<..<b}. ¬ P t› 
      by force
    show ?thesis 
      apply (rule finite_Psegments.insertI_2[of s0])
      subgoal using insertI_2.prems(2) local.insertI_2(1) by auto   
      subgoal using ‹s0 = a ∨ P s0› .
      subgoal using * .
      subgoal using ‹finite_Psegments P a s0› .
      done
  qed
  moreover note ‹s = b ∨ P s›  
  ultimately show ?case by auto
qed
 
subsection ‹Finite segment intersection of a path with the imaginary axis›

definition finite_ReZ_segments::"(real ⇒ complex) ⇒ complex ⇒ bool" where
  "finite_ReZ_segments g z = finite_Psegments (λt. Re (g t - z) = 0) 0 1"    

lemma finite_ReZ_segments_joinpaths:
  assumes g1:"finite_ReZ_segments g1 z" and g2: "finite_ReZ_segments g2 z" and
    "path g1" "path g2" "pathfinish g1=pathstart g2"
  shows "finite_ReZ_segments (g1+++g2) z" 
proof -
  define P where "P = (λt. (Re ((g1 +++ g2) t - z) = 0 ∧ 0<t ∧ t<1) ∨ t=0 ∨ t=1)"
  have "finite_Psegments P 0 (1/2)" 
  proof -
    have "finite_Psegments (λt. Re (g1 t - z) = 0) 0 1" 
      using g1 unfolding finite_ReZ_segments_def .
    then have "finite_Psegments (λt. Re (g1 (2 * t) - z) = 0) 0 (1/2)" 
      apply (drule_tac finite_Psegments_pos_linear[of _ 2 0 0 "1/2",simplified])
      by (auto simp add:comp_def)
    then show ?thesis
      unfolding P_def joinpaths_def
      by (elim finite_Psegments_congE,auto)
  qed
  moreover have "finite_Psegments P (1/2) 1" 
  proof -
    have "finite_Psegments (λt. Re (g2 t - z) = 0) 0 1" 
      using g2 unfolding finite_ReZ_segments_def .
    then have "finite_Psegments (λt. Re (g2 (2 * t-1) - z) = 0) (1/2) 1"  
      apply (drule_tac finite_Psegments_pos_linear[of _ 2 "1/2" "-1" 1,simplified])
      by (auto simp add:comp_def)
    then show ?thesis
      unfolding P_def joinpaths_def
      apply (elim finite_Psegments_congE)
      by auto
  qed  
  moreover have "closed {x. P x}"
  proof -
    define Q where "Q=(λt. Re ((g1 +++ g2) t - z) = 0)"
    have "continuous_on {0<..<1} (g1+++g2)"
      using path_join_imp[OF ‹path g1› ‹path g2› ‹pathfinish g1=pathstart g2›] 
      unfolding path_def by (auto elim:continuous_on_subset)
    from continuous_on_Re[OF this] have "continuous_on {0<..<1} (λx. Re ((g1 +++ g2) x))" .
    from continuous_on_open_Collect_neq[OF this,of "λ_. Re z",OF continuous_on_const,simplified]
    have "open {t. Re ((g1 +++ g2) t - z) ≠ 0 ∧ 0<t ∧ t<1}" 
       by (elim arg_elim[where f="open"],auto)
    from closed_Diff[of "{0::real..1}",OF _ this,simplified]
    show "closed {x. P x}" 
      apply (elim arg_elim[where f=closed])
      by (auto simp add:P_def)
  qed
  ultimately have "finite_Psegments P 0 1"
    using finite_Psegments_combine[of _ 0 "1/2" 1] by auto
  then show ?thesis 
    unfolding finite_ReZ_segments_def P_def
    by (elim finite_Psegments_congE,auto)
qed
      
lemma finite_ReZ_segments_congE:
  assumes "finite_ReZ_segments p1 z1" 
    "⋀t. ⟦0<t;t<1⟧ ⟹  Re(p1 t- z1) = Re(p2 t - z2)"
  shows "finite_ReZ_segments p2 z2"      
  using assms unfolding finite_ReZ_segments_def
  apply (elim finite_Psegments_congE)
  by auto 
       
lemma finite_ReZ_segments_constI:
  assumes "∀t. 0<t∧t<1 ⟶ g t = c"
  shows "finite_ReZ_segments g z" 
proof -
  have "finite_ReZ_segments (λ_. c) z" 
    unfolding finite_ReZ_segments_def 
    by (rule finite_Psegments_constI,auto)
  then show ?thesis using assms
    by (elim finite_ReZ_segments_congE,auto)
qed 

lemma finite_ReZ_segment_cases [consumes 1, case_names subEq subNEq,cases pred:finite_ReZ_segments]:
  assumes "finite_ReZ_segments g z"
    and subEq:"(⋀s. ⟦s ∈ {0..<1};s=0∨Re (g s) = Re z;
          ∀t∈{s<..<1}. Re (g t) = Re z;finite_ReZ_segments (subpath 0 s g) z⟧ ⟹ P)" 
    and subNEq:"(⋀s. ⟦s ∈ {0..<1};s=0∨Re (g s) = Re z;
          ∀t∈{s<..<1}. Re (g t) ≠ Re z;finite_ReZ_segments (subpath 0 s g) z⟧ ⟹ P)"
  shows "P"  
using assms(1) unfolding finite_ReZ_segments_def
proof (cases rule:finite_Psegments.cases)
  case emptyI
  then show ?thesis by auto
next
  case (insertI_1 s)
  have "finite_ReZ_segments (subpath 0 s g) z" 
  proof (cases "s=0")
    case True
    show ?thesis
      apply (rule finite_ReZ_segments_constI)
      using True unfolding subpath_def by auto
  next
    case False
    then have "s>0" using ‹s∈{0..<1}› by auto
    from finite_Psegments_pos_linear[OF _ this,of _ 0 0 1] insertI_1(4)
    show "finite_ReZ_segments (subpath 0 s g) z"
      unfolding finite_ReZ_segments_def comp_def subpath_def by auto
  qed  
  then show ?thesis using subEq insertI_1 by force
next
  case (insertI_2 s)
  have "finite_ReZ_segments (subpath 0 s g) z" 
  proof (cases "s=0")
    case True
    show ?thesis
      apply (rule finite_ReZ_segments_constI)
      using True unfolding subpath_def by auto
  next
    case False
    then have "s>0" using ‹s∈{0..<1}› by auto
    from finite_Psegments_pos_linear[OF _ this,of _ 0 0 1] insertI_2(4)
    show "finite_ReZ_segments (subpath 0 s g) z"
      unfolding finite_ReZ_segments_def comp_def subpath_def by auto
  qed
  then show ?thesis using subNEq insertI_2 by force
qed         
  
lemma finite_ReZ_segments_induct [case_names sub0 subEq subNEq, induct pred:finite_ReZ_segments]:
  assumes "finite_ReZ_segments g z"
  assumes  sub0:"⋀g z. (P (subpath 0 0 g) z)" 
    and subEq:"(⋀s g z. ⟦s ∈ {0..<1};s=0∨Re (g s) = Re z;
          ∀t∈{s<..<1}. Re (g t) = Re z;finite_ReZ_segments (subpath 0 s g) z; 
          P (subpath 0 s g) z⟧ ⟹ P g z)" 
    and subNEq:"(⋀s g z. ⟦s ∈ {0..<1};s=0∨Re (g s) = Re z;
          ∀t∈{s<..<1}. Re (g t) ≠ Re z;finite_ReZ_segments (subpath 0 s g) z;
          P (subpath 0 s g) z⟧ ⟹ P g z)"
  shows "P g z" 
proof -
  have "finite_Psegments (λt. Re (g t - z) = 0) 0 1" 
    using assms(1) unfolding finite_ReZ_segments_def by auto
  then have "(0::real)≤1 ⟶ P (subpath 0 1 g) z"
  proof (induct rule: finite_Psegments.induct[of _ 0 1 "λa b. b≥a ⟶ P (subpath a b g) z"] )
    case (emptyI a b)
    then show ?case using sub0[of "subpath a b g"] unfolding subpath_def by auto 
  next
    case (insertI_1 s a b)
    have ?case when "a=b"
      using sub0[of "subpath a b g"] that unfolding subpath_def by auto        
    moreover have ?case when "a≠b"
    proof -
      have "b>a" using that ‹s ∈ {a..<b}› by auto
      define s'::real where "s'=(s-a)/(b-a)"  
      have "P (subpath a b g) z" 
      proof (rule subEq[of s' "subpath a b g"])
        show "∀t∈{s'<..<1}. Re (subpath a b g t) = Re z" 
        proof 
          fix t assume "t ∈ {s'<..<1}"
          then have "(b - a) * t + a∈{s<..<b}" 
            unfolding s'_def using ‹b>a› ‹s ∈ {a..<b}›
            apply (auto simp add:field_simps)
            by (sos "((((A<0 * (A<1 * A<2)) * R<1) + (((A<=1 * (A<0 * R<1)) * (R<1 * [1]^2))
               + ((A<=0 * (A<0 * (A<1 * R<1))) * (R<1 * [1]^2)))))")  
          then have "Re (g ((b - a) * t + a) - z) = 0"
            using insertI_1(3)[rule_format,of "(b - a) * t + a"] by auto
          then show "Re (subpath a b g t) = Re z" 
            unfolding subpath_def by auto
        qed
        show "finite_ReZ_segments (subpath 0 s' (subpath a b g)) z"
        proof (cases "s=a")
          case True
          then show ?thesis unfolding s'_def subpath_def 
            by (auto intro:finite_ReZ_segments_constI)
        next
          case False
          have "finite_Psegments (λt. Re (g t - z) = 0) a s"
            using insertI_1(4) unfolding finite_ReZ_segments_def by auto
          then have "finite_Psegments ((λt. Re (g t - z) = 0) ∘ (λt. (s - a) * t + a)) 0 1" 
            apply (elim finite_Psegments_pos_linear[of _ "s-a" 0 a 1,simplified])
            using False ‹s∈{a..<b}› by auto
          then show ?thesis 
            using ‹b>a› unfolding finite_ReZ_segments_def subpath_def s'_def comp_def
            by auto
        qed
        show "s' ∈ {0..<1}"
          using ‹b>a› ‹s∈{a..<b}› unfolding s'_def 
          by (auto simp add:field_simps)
        show "P (subpath 0 s' (subpath a b g)) z"
        proof -
          have "P (subpath a s g) z" using insertI_1(1,5) by auto
          then show ?thesis 
            using ‹b>a› unfolding s'_def subpath_def  by simp  
        qed
        show "s' = 0 ∨ Re (subpath a b g s') = Re z"
        proof -
          have ?thesis when "s=a"
            using that unfolding s'_def by auto
          moreover have ?thesis when "Re (g s - z) = 0"
            using that unfolding s'_def subpath_def by auto
          ultimately show ?thesis using ‹s = a ∨ Re (g s - z) = 0› by auto
        qed
      qed
      then show ?thesis using ‹b>a› by auto
    qed
    ultimately show ?case by auto
  next
    case (insertI_2 s a b)
    have ?case when "a=b"
      using sub0[of "subpath a b g"] that unfolding subpath_def by auto        
    moreover have ?case when "a≠b"
    proof -
      have "b>a" using that ‹s ∈ {a..<b}› by auto
      define s'::real where "s'=(s-a)/(b-a)"  
      have "P (subpath a b g) z" 
      proof (rule subNEq[of s' "subpath a b g"])
        show "∀t∈{s'<..<1}. Re (subpath a b g t) ≠ Re z" 
        proof 
          fix t assume "t ∈ {s'<..<1}"
          then have "(b - a) * t + a∈{s<..<b}" 
            unfolding s'_def using ‹b>a› ‹s ∈ {a..<b}›
            apply (auto simp add:field_simps)
            by (sos "((((A<0 * (A<1 * A<2)) * R<1) + (((A<=1 * (A<0 * R<1)) * (R<1 * [1]^2)) + 
              ((A<=0 * (A<0 * (A<1 * R<1))) * (R<1 * [1]^2)))))")  
          then have "Re (g ((b - a) * t + a) - z) ≠ 0"
            using insertI_2(3)[rule_format,of "(b - a) * t + a"] by auto
          then show "Re (subpath a b g t) ≠ Re z" 
            unfolding subpath_def by auto
        qed
        show "finite_ReZ_segments (subpath 0 s' (subpath a b g)) z"
        proof (cases "s=a")
          case True
          then show ?thesis unfolding s'_def subpath_def 
            by (auto intro:finite_ReZ_segments_constI)
        next
          case False
          have "finite_Psegments (λt. Re (g t - z) = 0) a s"
            using insertI_2(4) unfolding finite_ReZ_segments_def by auto
          then have "finite_Psegments ((λt. Re (g t - z) = 0) ∘ (λt. (s - a) * t + a)) 0 1" 
            apply (elim finite_Psegments_pos_linear[of _ "s-a" 0 a 1,simplified])
            using False ‹s∈{a..<b}› by auto
          then show ?thesis 
            using ‹b>a› unfolding finite_ReZ_segments_def subpath_def s'_def comp_def
            by auto
        qed
        show "s' ∈ {0..<1}"
          using ‹b>a› ‹s∈{a..<b}› unfolding s'_def 
          by (auto simp add:field_simps)
        show "P (subpath 0 s' (subpath a b g)) z"
        proof -
          have "P (subpath a s g) z" using insertI_2(1,5) by auto
          then show ?thesis 
            using ‹b>a› unfolding s'_def subpath_def  by simp  
        qed
        show "s' = 0 ∨ Re (subpath a b g s') = Re z"
        proof -
          have ?thesis when "s=a"
            using that unfolding s'_def by auto
          moreover have ?thesis when "Re (g s - z) = 0"
            using that unfolding s'_def subpath_def by auto
          ultimately show ?thesis using ‹s = a ∨ Re (g s - z) = 0› by auto
        qed
      qed
      then show ?thesis using ‹b>a› by auto
    qed
    ultimately show ?case by auto
  qed
  then show ?thesis by auto
qed

lemma finite_ReZ_segments_shiftpah:
  assumes "finite_ReZ_segments g z" "s∈{0..1}" "path g" and loop:"pathfinish g = pathstart g" 
  shows "finite_ReZ_segments (shiftpath s g) z"
proof -
  have "finite_Psegments (λt. Re (shiftpath s g t - z) = 0) 0 (1-s)"
  proof -
    have "finite_Psegments (λt. Re (g t) = Re z) s 1" 
      using assms finite_Psegments_included[of _ 0 1 s] unfolding finite_ReZ_segments_def  
      by force   
    then have "finite_Psegments (λt. Re (g (s + t) - z) = 0) 0 (1-s)" 
      using finite_Psegments_pos_linear[of "λt. Re (g t - z) =0" 1 0 s "1-s",simplified]
      unfolding comp_def by (auto simp add:algebra_simps)
    then show ?thesis unfolding shiftpath_def
      apply (elim finite_Psegments_congE)
      using ‹s∈{0..1}› by auto  
  qed
  moreover have "finite_Psegments (λt. Re (shiftpath s g t - z) = 0) (1-s) 1"  
  proof -
    have "finite_Psegments (λt. Re (g t) = Re z) 0 s " 
      using assms finite_Psegments_included unfolding finite_ReZ_segments_def  
      by force   
    then have "finite_Psegments (λt. Re (g (s + t - 1) - z) = 0) (1-s) 1" 
      using finite_Psegments_pos_linear[of "λt. Re (g t - z) =0" 1 "1-s" "s-1" 1,simplified]
      unfolding comp_def by (auto simp add:algebra_simps)
    then show ?thesis unfolding shiftpath_def
      apply (elim finite_Psegments_congE)
      using ‹s∈{0..1}› by auto  
  qed
  moreover have "1 - s ∈ {0..1}" using ‹s∈{0..1}› by auto
  moreover have "closed ({x. Re (shiftpath s g x - z) = 0} ∩ {0..1})"
  proof -
    let ?f = "λx. Re (shiftpath s g x - z)"  
    have "continuous_on {0..1} ?f"
      using path_shiftpath[OF ‹path g› loop ‹s∈{0..1}›] unfolding path_def
      by (auto intro: continuous_intros)
    from continuous_closed_preimage_constant[OF this,of 0,simplified] 
    show ?thesis 
      apply (elim arg_elim[of closed])
      by force
  qed
  ultimately show ?thesis unfolding finite_ReZ_segments_def 
    by (rule finite_Psegments_combine[where b="1-s"])  
qed
     
lemma finite_imp_finite_ReZ_segments:
  assumes "finite {t. Re (g t - z) = 0 ∧ 0 ≤ t ∧ t≤1}"
  shows "finite_ReZ_segments g z"
proof -
  define P where "P = (λt. Re (g t - z) = 0)"
  define rs where "rs=(λb. {t. P t ∧ 0 < t ∧ t<b})"
  have "finite_Psegments P 0 b" when "finite (rs b)" "b>0" for b
  using that
  proof (induct "card (rs b)" arbitrary:b rule:nat_less_induct)
    case ind:1
    have ?case when "rs b= {}"
      apply (rule finite_Psegments.intros(3)[of 0])
      using that ‹0 < b› unfolding rs_def by (auto intro:finite_Psegments.intros)  
    moreover have ?case when "rs b≠{}"
    proof -
      define lj where "lj = Max (rs b)" 
      have "0<lj" "lj<b" "P lj"
        using Max_in[OF ‹finite (rs b)› ‹rs b≠{}›,folded lj_def]
        unfolding rs_def by auto
      show ?thesis 
      proof (rule finite_Psegments.intros(3)[of lj])
        show "lj ∈ {0..<b}" " lj = 0 ∨ P lj" 
          using ‹0<lj› ‹lj<b› ‹P lj› by auto
        show "∀t∈{lj<..<b}. ¬ P t"
        proof (rule ccontr)
          assume " ¬ (∀t∈{lj<..<b}. ¬ P t) "
          then obtain t where t:"P t" "lj < t" "t < b" by auto
          then have "t∈rs b" unfolding rs_def using ‹lj>0› by auto
          then have "t≤lj" using Max_ge[OF ‹finite (rs b)›,of t] unfolding lj_def by auto
          then show False using ‹t>lj› by auto
        qed
        show "finite_Psegments P 0 lj"
        proof (rule ind.hyps[rule_format,of "card (rs lj)" lj,simplified])
          show "finite (rs lj)"
            using ‹finite (rs b)› unfolding rs_def using ‹lj<b› 
            by (auto elim!:rev_finite_subset )
          show "card (rs lj) < card (rs b)"
            apply (rule psubset_card_mono[OF ‹finite (rs b)›])
            using Max_in ‹finite (rs lj)› ‹lj < b› lj_def rs_def that by fastforce
          show "0 < lj" using ‹0<lj› .
        qed
      qed
    qed
    ultimately show ?case by auto 
  qed
  moreover have "finite (rs 1)"
    using assms unfolding rs_def P_def
    by (auto elim:rev_finite_subset)
  ultimately have "finite_Psegments P 0 1" by auto
  then show ?thesis unfolding P_def finite_ReZ_segments_def .
qed
  
lemma finite_ReZ_segments_poly_linepath:
  shows "finite_ReZ_segments (poly p o linepath a b) z" 
proof -
  define P where "P=map_poly Re (pcompose (p-[:z:]) [:a,b-a:])"
  have *:"Re ((poly p ∘ linepath a b) t - z) = 0 ⟷ poly P t=0" for t
    unfolding inner_complex_def P_def linepath_def comp_def
    apply (subst Re_poly_of_real[symmetric])
    by (auto simp add: algebra_simps poly_pcompose scaleR_conv_of_real)
  have ?thesis when "P≠0"
  proof -
    have "finite {t. poly P t=0}" using that poly_roots_finite by auto
    then have "finite {t. Re ((poly p ∘ linepath a b) t - z) = 0 ∧ 0 ≤ t ∧ t ≤ 1}"
      using *
      by auto
    then show ?thesis   
      using finite_imp_finite_ReZ_segments[of "poly p o linepath a b" z] by auto
  qed
  moreover have ?thesis when "P=0"
    unfolding finite_ReZ_segments_def
    apply (rule finite_Psegments_constI[where c=True])  
    apply (subst *)
    using that by auto 
  ultimately show ?thesis by auto
qed  
  
lemma part_circlepath_half_finite_inter:
  assumes "st≠tt" "r≠0" "c≠0"
  shows "finite {t. part_circlepath z0 r st tt t ∙ c = d ∧ 0≤ t ∧ t≤1}" (is "finite ?T")
proof -
  let ?S = "{θ. (z0+r*exp (𝗂 * θ )) ∙ c = d ∧ θ ∈ closed_segment st tt}"
  define S where "S ≡ {θ. (z0+r*exp (𝗂 * θ )) ∙ c = d ∧ θ ∈ closed_segment st tt}"
  have "S = linepath st tt ` ?T"
  proof   
    define g where "g≡(λt. (t-st)/(tt -st))"
    have "0≤g t" "g t≤1" when "t ∈ closed_segment st tt " for t
      using that ‹st≠tt› closed_segment_eq_real_ivl unfolding  g_def real_scaleR_def
      by (auto simp add:divide_simps)
    moreover have "linepath st tt (g t) =t" "g (linepath st tt t) = t" for t
      unfolding linepath_def g_def real_scaleR_def using ‹st≠tt›
      apply (simp_all add:divide_simps)
      by (auto simp add:algebra_simps )
    ultimately have "x∈linepath st tt ` ?T" when "x∈S" for x
      using that unfolding S_def 
      by (auto intro!:image_eqI[where x="g x"] simp add:part_circlepath_def)
    then show "S ⊆ linepath st tt ` ?T" by auto
  next
    have "x∈S" when "x∈linepath st tt ` ?T" for x
      using that unfolding part_circlepath_def S_def
      by (auto simp add: linepath_in_path)
    then show "linepath st tt ` ?T ⊆ S" by auto
  qed
  moreover have "finite S" 
  proof -
    define a' b' c' where "a'=r * Re c" and "b' = r* Im c" and "c'=Im c * Im z0 + Re z0 * Re c - d"
    define f where "f θ= a' * cos θ + b' * sin θ + c'" for θ
    have "(z0+r*exp (𝗂 * θ )) ∙ c = d ⟷ f θ = 0" for θ
      unfolding exp_Euler inner_complex_def f_def a'_def b'_def c'_def
      by (auto simp add:algebra_simps cos_of_real sin_of_real)
    then have *:"S = roots f ∩ closed_segment st tt"
      unfolding S_def roots_within_def by auto
    have "uniform_discrete S"
    proof -
      have "a' ≠ 0 ∨ b' ≠ 0 ∨ c' ≠ 0" 
        using assms complex_eq_iff unfolding a'_def b'_def c'_def 
        by auto
      then have "periodic_set (roots f) (4 * pi)"
        using periodic_set_sin_cos_linear[of a' b' c',folded f_def] by auto
      then have "uniform_discrete (roots f)" using periodic_imp_uniform_discrete by auto
      then show ?thesis unfolding * by auto
    qed
    moreover have "bounded S" unfolding * 
      by (simp add: bounded_Int bounded_closed_segment)
    ultimately show ?thesis using uniform_discrete_finite_iff by auto
  qed
  moreover have "inj_on (linepath st tt) ?T" 
  proof -
    have "inj (linepath st tt)"
      unfolding linepath_def using assms inj_segment by blast
    then show ?thesis by (auto elim:subset_inj_on)
  qed
  ultimately show ?thesis by (auto elim!: finite_imageD)
qed

lemma linepath_half_finite_inter:
  assumes "a ∙ c ≠ d ∨ b ∙ c ≠ d"
  shows "finite {t. linepath a b t ∙ c = d ∧ 0≤ t ∧ t≤1}" (is "finite ?S")
proof (rule ccontr)
  assume asm:"infinite ?S"
  obtain t1 t2 where u1u2:"t1≠t2" "t1∈?S" "t2∈?S"
  proof -
    obtain t1 where "t1∈?S" using not_finite_existsD asm by blast
    moreover have "∃u2. u2∈?S-{t1}" 
      using infinite_remove[OF asm,of t1] 
      by (meson finite.emptyI rev_finite_subset subsetI)
    ultimately show ?thesis using that by auto
  qed
  have t1:"(1-t1)*(a ∙ c) + t1 * (b ∙ c) = d"
    using ‹t1∈?S› unfolding linepath_def by (simp add: inner_left_distrib)
  have t2:"(1-t2)*(a ∙ c) + t2 * (b ∙ c) = d"
    using ‹t2∈?S› unfolding linepath_def by (simp add: inner_left_distrib)
  have "a ∙ c = d"
  proof -
    have "t2*((1-t1)*(a ∙ c) + t1 * (b ∙ c)) = t2*d" using t1 by auto
    then have *:"(t2-t1*t2)*(a ∙ c) + t1*t2 * (b ∙ c) = t2*d" by (auto simp add:algebra_simps)
    have "t1*((1-t2)*(a ∙ c) + t2 * (b ∙ c)) = t1*d" using t2 by auto
    then have **:"(t1-t1*t2)*(a ∙ c) + t1*t2 * (b ∙ c) = t1*d" by (auto simp add:algebra_simps)
    have "(t2-t1)*(a ∙ c) = (t2-t1)*d" using arg_cong2[OF * **,of minus]
      by (auto simp add:algebra_simps)
    then show ?thesis using ‹t1≠t2› by auto
  qed
  moreover have "b ∙ c = d"
  proof -
    have "(1-t2)*((1-t1)*(a ∙ c) + t1 * (b ∙ c)) = (1-t2)*d" using t1 by auto
    then have *:"(1-t1)*(1-t2)*(a ∙ c) + (t1-t1*t2) * (b ∙ c) = (1-t2)*d" by (auto simp add:algebra_simps)
    have "(1-t1)*((1-t2)*(a ∙ c) + t2 * (b ∙ c)) = (1-t1)*d" using t2 by auto
    then have **:"(1-t1)*(1-t2)*(a ∙ c) + (t2-t1*t2) * (b ∙ c) = (1-t1)*d" by (auto simp add:algebra_simps)
    have "(t2-t1)*(b ∙ c) = (t2-t1)*d" using arg_cong2[OF ** *,of minus]
      by (auto simp add:algebra_simps)
    then show ?thesis using ‹t1≠t2› by auto
  qed
  ultimately show False using assms by auto  
qed
  
lemma finite_half_joinpaths_inter:
  assumes "finite {t. l1 t ∙ c = d ∧ 0≤ t ∧ t≤1}" "finite {t. l2 t ∙ c = d ∧ 0≤ t ∧ t≤1}"
  shows "finite {t. (l1+++l2) t ∙ c = d ∧ 0≤ t ∧ t≤1}"
proof -
  let ?l1s = "{t. l1 (2*t) ∙ c = d ∧ 0≤ t ∧ t≤1/2}"
  let ?l2s = "{t. l2 (2 * t - 1) ∙ c = d ∧ 1/2< t ∧ t≤1}"
  let ?ls = "λl. {t. l t ∙ c = d ∧ 0≤ t ∧ t≤1}"
  have "{t. (l1+++l2) t ∙ c = d ∧ 0≤ t ∧ t≤1} = ?l1s ∪ ?l2s"
    unfolding joinpaths_def by auto
  moreover have "finite ?l1s"
  proof -
    have "?l1s = ((*) (1/2)) ` ?ls l1" by (auto intro:rev_image_eqI)
    thus ?thesis using assms by simp 
  qed
  moreover have "finite ?l2s"
  proof -
    have "?l2s ⊆ (λx. x/2 + 1/2) ` ?ls l2" by (auto intro:rev_image_eqI simp add:field_simps)
    thus ?thesis using assms 
      by (auto elim:finite_subset)
  qed
  ultimately show ?thesis by simp
qed  
  
lemma finite_ReZ_segments_linepath:
  "finite_ReZ_segments (linepath a b) z"
proof -
  have ?thesis when "Re a≠Re z ∨ Re b ≠Re z"
  proof -
    let ?S1="{t. Re (linepath a b t-z) = 0 ∧ 0 ≤ t ∧ t ≤ 1}"
    have "finite ?S1" 
      using linepath_half_finite_inter[of a "Complex 1 0" "Re z" b] that 
      using one_complex.code by auto
    from finite_imp_finite_ReZ_segments[OF this] show ?thesis .
  qed
  moreover have ?thesis when "Re a=Re z" "Re b=Re z"
    unfolding finite_ReZ_segments_def
    apply (rule finite_Psegments.intros(2)[of 0])
    using that unfolding linepath_def by (auto simp add:algebra_simps intro:finite_Psegments.intros)
  ultimately show ?thesis by blast
qed
  
lemma finite_ReZ_segments_part_circlepath:
  "finite_ReZ_segments (part_circlepath z0 r st tt) z"
proof -
  have ?thesis when "st ≠ tt" "r ≠ 0"
  proof -
    let ?S1="{t. Re (part_circlepath z0 r st tt t-z) = 0 ∧ 0 ≤ t ∧ t ≤ 1}"  
    have "finite ?S1"
      using part_circlepath_half_finite_inter[of st tt r "Complex 1 0" z0 "Re z"] that one_complex.code
      by (auto simp add:inner_complex_def )
    from finite_imp_finite_ReZ_segments[OF this] show ?thesis .
  qed
  moreover have ?thesis when "st =tt ∨ r=0"
  proof -
    define c where "c = z0 + r * exp (𝗂 *  tt)"
    have "part_circlepath z0 r st tt = (λt. c)"
      unfolding part_circlepath_def c_def using that linepath_refl by auto
    then show ?thesis 
      using finite_ReZ_segments_linepath[of c c z] linepath_refl[of c]
      by auto
  qed
  ultimately show ?thesis by blast
qed
   
lemma finite_ReZ_segments_poly_of_real:
  shows "finite_ReZ_segments (poly p o of_real) z" 
  using finite_ReZ_segments_poly_linepath[of p 0 1 z] unfolding linepath_def
  by (auto simp add:scaleR_conv_of_real)
 
lemma finite_ReZ_segments_subpath:
  assumes "finite_ReZ_segments g z"
    "0≤u" "u≤v" "v≤1"
  shows "finite_ReZ_segments (subpath u v g) z" 
proof (cases "u=v")
  case True  
  then show ?thesis 
    unfolding subpath_def by (auto intro:finite_ReZ_segments_constI)
next
  case False
  then have "u<v" using ‹u≤v› by auto
  define P where "P=(λt. Re (g t - z) = 0)"
  have "finite_ReZ_segments (subpath u v g) z 
      = finite_Psegments (P o (λt. (v - u) * t + u)) 0 1"
    unfolding finite_ReZ_segments_def subpath_def P_def comp_def by auto
  also have "..."
    apply (rule finite_Psegments_pos_linear)
    using assms False unfolding finite_ReZ_segments_def
    by (fold P_def,auto elim:finite_Psegments_included)        
  finally show ?thesis .
qed   
  
subsection ‹jump and jumpF› 
  
definition jump::"(real ⇒ real) ⇒ real ⇒ int" where
  "jump f a = (if 
        (LIM x (at_left a). f x :> at_bot) ∧ (LIM x (at_right a). f x :> at_top) 
      then 1 else if 
        (LIM x (at_left a). f x :> at_top) ∧ (LIM x (at_right a). f x :> at_bot) 
      then -1 else 0)"
  
definition jumpF::"(real ⇒ real) ⇒ real filter ⇒ real" where 
  "jumpF f F ≡ (if filterlim f at_top F then 1/2 else 
    if filterlim f at_bot F then -1/2 else (0::real))"
   
lemma jumpF_const[simp]:
  assumes "F≠bot"
  shows "jumpF (λ_. c) F = 0" 
proof -
  have False when "LIM x F. c :> at_bot"
    using filterlim_at_bot_nhds[OF that _ ‹F≠bot›] by auto
  moreover have False when "LIM x F. c :> at_top"
    using filterlim_at_top_nhds[OF that _ ‹F≠bot›] by auto
  ultimately show ?thesis unfolding jumpF_def by auto
qed

lemma jumpF_not_infinity:
  assumes "continuous F g" "F≠bot"
  shows "jumpF g F = 0"  
proof -
  have "¬ filterlim g at_infinity F"
    using not_tendsto_and_filterlim_at_infinity[OF ‹F ≠bot› assms(1)[unfolded continuous_def]] 
    by auto
  then have "¬ filterlim g at_bot F" "¬ filterlim g at_top F"
    using at_bot_le_at_infinity at_top_le_at_infinity filterlim_mono by blast+
  then show ?thesis unfolding jumpF_def by auto
qed
  
lemma jumpF_linear_comp:
  assumes "c≠0"
  shows 
    "jumpF (f o (λx. c*x+b)) (at_left x) = 
            (if c>0 then jumpF f (at_left (c*x+b)) else jumpF f (at_right (c*x+b)))"
    (is ?case1)
    "jumpF (f o (λx. c*x+b)) (at_right x) = 
            (if c>0 then jumpF f (at_right (c*x+b)) else jumpF f (at_left (c*x+b)))"
    (is ?case2)
proof -
  let ?g = "λx. c*x+b"  
  have ?case1 ?case2 when "¬ c>0"
  proof -
    have "c<0" using ‹c≠0› that by auto
    have "filtermap ?g (at_left x) = at_right (?g x)"
         "filtermap ?g (at_right x) = at_left (?g x)"
      using ‹c<0› 
      filtermap_linear_at_left[OF ‹c≠0›, of b x] 
      filtermap_linear_at_right[OF ‹c≠0›, of b x] by auto
    then have 
        "jumpF (f ∘ ?g) (at_left x) = jumpF f (at_right (?g x))"
        "jumpF (f ∘ ?g) (at_right x) = jumpF f (at_left (?g x))"
      unfolding jumpF_def filterlim_def comp_def
      by (auto simp add: filtermap_filtermap[of f ?g,symmetric])
    then show ?case1 ?case2 using ‹c<0› by auto
  qed
  moreover have ?case1 ?case2 when "c>0"
  proof -
    have "filtermap ?g (at_left x) = at_left (?g x)"
         "filtermap ?g (at_right x) = at_right (?g x)"
      using that 
      filtermap_linear_at_left[OF ‹c≠0›, of b x] 
      filtermap_linear_at_right[OF ‹c≠0›, of b x] by auto
    then have 
        "jumpF (f ∘ ?g) (at_left x) = jumpF f (at_left (?g x))"
        "jumpF (f ∘ ?g) (at_right x) = jumpF f (at_right (?g x))"
      unfolding jumpF_def filterlim_def comp_def
      by (auto simp add: filtermap_filtermap[of f ?g,symmetric])
    then show ?case1 ?case2 using that by auto
  qed
  ultimately show ?case1 ?case2 by auto
qed  
  
lemma jump_const[simp]:"jump (λ_. c) a = 0"
proof -
  have False when "LIM x (at_left a). c :> at_bot"
    apply (rule not_tendsto_and_filterlim_at_infinity[of "at_left a" "λ_. c" c])
      apply auto
    using at_bot_le_at_infinity filterlim_mono that by blast
  moreover have False when "LIM x (at_left a). c :> at_top"
    apply (rule not_tendsto_and_filterlim_at_infinity[of "at_left a" "λ_. c" c])
      apply auto
    using at_top_le_at_infinity filterlim_mono that by blast  
  ultimately show ?thesis unfolding jump_def by auto
qed  

lemma jump_not_infinity:
  "isCont f a ⟹ jump f a =0"
  by (meson at_bot_le_at_infinity at_top_le_at_infinity filterlim_at_split 
      filterlim_def isCont_def jump_def not_tendsto_and_filterlim_at_infinity 
      order_trans trivial_limit_at_left_real) 
  
lemma jump_jump_poly_aux:
  assumes "p≠0" "coprime p q"
  shows "jump (λx. poly q x / poly p x) a = jump_poly q p a"
proof (cases "q=0")
  case True
  then show ?thesis by auto
next
  case False
  define f where "f ≡ (λx. poly q x / poly p x)"
  have ?thesis when "poly q a = 0"
  proof -
    have "poly p a≠0" using coprime_poly_0[OF ‹coprime p q›] that by blast
    then have "isCont f a" unfolding f_def by simp
    then have "jump f a=0" using jump_not_infinity by auto
    moreover have "jump_poly q p a=0"
      using jump_poly_not_root[OF ‹poly p a≠0›] by auto
    ultimately show ?thesis unfolding f_def by auto
  qed
  moreover have ?thesis when "poly q a≠0"
  proof (cases "even(order a p)")
    case True
    define c where "c≡sgn (poly q a)"
    note 
      filterlim_divide_at_bot_at_top_iff
        [OF _ that,of "poly q"  "at_left a" "poly p",folded f_def c_def,simplified]
      filterlim_divide_at_bot_at_top_iff
        [OF _ that,of "poly q"  "at_right a" "poly p",folded f_def c_def,simplified]
    moreover have "(poly p has_sgnx - c) (at_left a) = (poly p has_sgnx - c) (at_right a)"
         "(poly p has_sgnx c) (at_left a) = (poly p has_sgnx c) (at_right a)"
      using poly_has_sgnx_left_right[OF ‹p≠0›] True by auto
    moreover have "c≠0" by (simp add: c_def sgn_if that)
    then have False when 
        "(poly p has_sgnx - c) (at_right a)" 
        "(poly p has_sgnx c) (at_right a)"
      using has_sgnx_unique[OF _ that] by auto
    ultimately have "jump f a = 0"
      unfolding jump_def by auto
    moreover have "jump_poly q p a = 0" unfolding jump_poly_def
      using True by (simp add: order_0I that)
    ultimately show ?thesis unfolding f_def by auto
  next
    case False
    define c where "c≡sgn (poly q a)"
    have "(poly p ⤏ 0) (at a)" using False 
      by (metis even_zero order_0I poly_tendsto(1))
    then have "(poly p ⤏ 0) (at_left a)" and "(poly p ⤏ 0) (at_right a)"
      by (auto simp add: filterlim_at_split)
    moreover note 
      filterlim_divide_at_bot_at_top_iff
        [OF _ that,of "poly q" _ "poly p",folded f_def c_def]
    moreover have "(poly p has_sgnx c) (at_left a) = (poly p has_sgnx - c) (at_right a)"
         "(poly p has_sgnx - c) (at_left a) = (poly p has_sgnx c) (at_right a)"
      using poly_has_sgnx_left_right[OF ‹p≠0›] False by auto
    ultimately have "jump f a = (if (poly p has_sgnx c) (at_right a) then 1
        else if (poly p has_sgnx - c) (at_right a) then -1 else 0)"
      unfolding jump_def by auto
    also have "... = (if sign_r_pos (q * p) a then 1 else - 1)"
    proof -
      have "(poly p has_sgnx c) (at_right a) ⟷  sign_r_pos (q * p) a " 
      proof 
        assume "(poly p has_sgnx c) (at_right a)"
        then have "sgnx (poly p) (at_right a) = c" by auto
        moreover have "sgnx (poly q) (at_right a) = c"
          unfolding c_def using that by (auto intro!: tendsto_nonzero_sgnx)
        ultimately have "sgnx (λx. poly (q*p) x) (at_right a) = c * c"
          by (simp add:sgnx_times)
        moreover have "c≠0" by (simp add: c_def sgn_if that) 
        ultimately have "sgnx (λx. poly (q*p) x) (at_right a) > 0"
          using not_real_square_gt_zero by fastforce
        then show "sign_r_pos (q * p) a" using sign_r_pos_sgnx_iff 
          by blast
      next
        assume asm:"sign_r_pos (q * p) a"
        let ?c1 = "sgnx (poly p) (at_right a)"
        let ?c2 = "sgnx (poly q) (at_right a)"
        have "0 < sgnx (λx. poly (q * p) x) (at_right a)"
          using asm sign_r_pos_sgnx_iff by blast
        then have "?c2 * ?c1 >0" 
          apply (subst (asm) poly_mult)
          apply (subst (asm) sgnx_times)
          by auto
        then have "?c2>0 ∧ ?c1>0 ∨ ?c2<0 ∧ ?c1<0"
          by (simp add: zero_less_mult_iff)
        then have "?c1=?c2"
          using sgnx_values[OF sgnx_able_poly(1), of a,simplified]
          by (metis add.inverse_neutral less_minus_iff less_not_sym)    
        moreover have "sgnx (poly q) (at_right a) = c"
          unfolding c_def using that by (auto intro!: tendsto_nonzero_sgnx)
        ultimately have "?c1 = c" by auto
        then show "(poly p has_sgnx c) (at_right a)"
          using sgnx_able_poly(1) sgnx_able_sgnx by blast
      qed  
      then show ?thesis 
        unfolding jump_poly_def using poly_has_sgnx_values[OF ‹p≠0›]
        by (metis add.inverse_inverse c_def sgn_if that)
    qed
    also have "... = jump_poly q p a"
      unfolding jump_poly_def using False order_root that by (simp add: order_root assms(1))
    finally show ?thesis unfolding f_def by auto
  qed
  ultimately show ?thesis by auto
qed
 
lemma jump_jumpF:
  assumes cont:"isCont (inverse o f) a" and 
      sgnxl:"(f has_sgnx l) (at_left a)" and sgnxr:"(f has_sgnx r) (at_right a)" and
      "l≠0 " "r≠0"
  shows "jump f a = jumpF f (at_right a) - jumpF f (at_left a)"
proof -
  have ?thesis when "filterlim f at_bot (at_left a)" "filterlim f at_top (at_right a)"
    unfolding jump_def jumpF_def 
    using that filterlim_at_top_at_bot[OF _ _ trivial_limit_at_left_real]
    by auto
  moreover have ?thesis when "filterlim f at_top (at_left a)" "filterlim f at_bot (at_right a)"
    unfolding jump_def jumpF_def 
    using that filterlim_at_top_at_bot[OF _ _ trivial_limit_at_right_real]
    by auto
  moreover have ?thesis when 
          "¬ filterlim f at_bot (at_left a) ∨ ¬ filterlim f at_top (at_right a)"
          "¬ filterlim f at_top (at_left a) ∨ ¬ filterlim f at_bot (at_right a)"
  proof (cases "f a=0")
    case False
    have "jumpF f (at_right a) = 0" "jumpF f (at_left a) = 0"
    proof -
      have "isCont (inverse o inverse o f) a" using cont False unfolding comp_def
        by (rule_tac continuous_at_within_inverse, auto)
      then have "isCont f a" unfolding comp_def by auto
      then have "(f ⤏ f a) (at_right a)" "(f ⤏ f a) (at_left a)"
        unfolding continuous_at_split by (auto simp add:continuous_within)
      moreover note trivial_limit_at_left_real trivial_limit_at_right_real
      ultimately show "jumpF f (at_right a) = 0" "jumpF f (at_left a) = 0"
        unfolding jumpF_def using filterlim_at_bot_nhds filterlim_at_top_nhds
        by metis+
    qed
    then show ?thesis unfolding jump_def using that by auto
  next
    case True
    then have tends0:"((λx. inverse (f x)) ⤏ 0) (at a)" 
      using cont unfolding isCont_def comp_def by auto
    have "jump f a = 0" using that unfolding jump_def by auto
    have r_lim:"if r>0 then filterlim f at_top (at_right a) else filterlim f at_bot (at_right a)"
    proof (cases "r>0")
      case True 
      then have "∀F x in (at_right a). 0 < f x" 
          using sgnxr unfolding has_sgnx_def
          by (auto elim:eventually_mono)
      then have "filterlim f at_top (at_right a)" 
        using filterlim_inverse_at_top[of "λx. inverse (f x)", simplified] tends0
        unfolding filterlim_at_split by auto
      then show ?thesis using True by presburger
    next
      case False
      then have "∀F x in (at_right a). 0 > f x" 
        using sgnxr ‹r≠0› False unfolding has_sgnx_def
        apply (elim eventually_mono)
        by (meson linorder_neqE_linordered_idom sgn_less)
      then have "filterlim f at_bot (at_right a)" 
        using filterlim_inverse_at_bot[of "λx. inverse (f x)", simplified] tends0
        unfolding filterlim_at_split by auto
      then show ?thesis using False by simp
    qed
    have l_lim:"if l>0 then filterlim f at_top (at_left a) else filterlim f at_bot (at_left a)"
    proof (cases "l>0")
      case True 
      then have "∀F x in (at_left a). 0 < f x" 
          using sgnxl unfolding has_sgnx_def
          by (auto elim:eventually_mono)
      then have "filterlim f at_top (at_left a)" 
        using filterlim_inverse_at_top[of "λx. inverse (f x)", simplified] tends0
        unfolding filterlim_at_split by auto
      then show ?thesis using True by presburger
    next
      case False
      then have "∀F x in (at_left a). 0 > f x" 
        using sgnxl ‹l≠0› False unfolding has_sgnx_def
        apply (elim eventually_mono)
        by (meson linorder_neqE_linordered_idom sgn_less)
      then have "filterlim f at_bot (at_left a)" 
        using filterlim_inverse_at_bot[of "λx. inverse (f x)", simplified] tends0
        unfolding filterlim_at_split by auto
      then show ?thesis using False by simp
    qed
      
    have ?thesis when "l>0" "r>0"
      using that l_lim r_lim ‹jump f a=0› unfolding jumpF_def by auto
    moreover have ?thesis when "¬ l>0" "¬ r>0"
    proof -
      have "filterlim f at_bot (at_right a)" "filterlim f at_bot (at_left a)" 
        using r_lim l_lim that by auto
      moreover then have "¬ filterlim f at_top (at_right a)" "¬ filterlim f at_top (at_left a)"
        by (auto elim: filterlim_at_top_at_bot)
      ultimately have "jumpF f (at_right a) = -1/2 "  "jumpF f (at_left a) = -1/2"
        unfolding jumpF_def by auto
      then show ?thesis using ‹jump f a=0› by auto
    qed
    moreover have ?thesis when "l>0" "¬ r>0"
    proof -
      note ‹¬ filterlim f at_top (at_left a) ∨ ¬ filterlim f at_bot (at_right a)›
      moreover have "filterlim f at_bot (at_right a)" "filterlim f at_top (at_left a)" 
        using r_lim l_lim that by auto
      ultimately have False by auto
      then show ?thesis by auto
    qed
    moreover have ?thesis when "¬ l>0" "r>0"
    proof -
      note ‹¬ filterlim f at_bot (at_left a) ∨ ¬ filterlim f at_top (at_right a)›
      moreover have "filterlim f at_bot (at_left a)" "filterlim f at_top (at_right a)" 
        using r_lim l_lim that by auto
      ultimately have False by auto
      then show ?thesis by auto
    qed
    ultimately show ?thesis by auto
  qed
  ultimately show ?thesis by auto
qed
  
lemma jump_linear_comp:
  assumes "c≠0"
  shows "jump (f o (λx. c*x+b)) x = (if c>0 then jump f (c*x+b) else -jump f (c*x+b))"
proof (cases "c>0")
  case False
  then have "c<0" using ‹c≠0› by auto
  let ?g = "λx. c*x+b"  
  have "filtermap ?g (at_left x) = at_right (?g x)"
       "filtermap ?g (at_right x) = at_left (?g x)"
    using ‹c<0› 
      filtermap_linear_at_left[OF ‹c≠0›, of b x] 
      filtermap_linear_at_right[OF ‹c≠0›, of b x] by auto
  then have "jump (f ∘ ?g) x = - jump f (c * x + b)"
    unfolding jump_def filterlim_def comp_def
    apply (auto simp add: filtermap_filtermap[of f ?g,symmetric])
    apply (fold filterlim_def)
    by (auto elim:filterlim_at_top_at_bot)
  then show ?thesis using ‹c<0› by auto
next
  case True
  let ?g = "λx. c*x+b"  
  have "filtermap ?g (at_left x) = at_left (?g x)"
       "filtermap ?g (at_right x) = at_right (?g x)"
    using True 
      filtermap_linear_at_left[OF ‹c≠0›, of b x] 
      filtermap_linear_at_right[OF ‹c≠0›, of b x] by auto
  then have "jump (f ∘ ?g) x = jump f (c * x + b)"
    unfolding jump_def filterlim_def comp_def
    by (auto simp add: filtermap_filtermap[of f ?g,symmetric])
  then show ?thesis using True by auto
qed 
  
lemma jump_divide_derivative:
  assumes "isCont f x" "g x = 0" "f x≠0" 
    and g_deriv:"(g has_field_derivative c) (at x)" and "c≠0"
  shows "jump (λt. f t/g t) x = (if sgn c = sgn ( f x) then 1 else -1)"  
proof -
  have g_tendsto:"(g ⤏ 0) (at_left x)" "(g ⤏ 0) (at_right x)"
    by (metis DERIV_isCont Lim_at_imp_Lim_at_within assms(2) assms(4) continuous_at)+
  have f_tendsto:"(f ⤏ f x) (at_left x)" "(f ⤏ f x) (at_right x)"
    using Lim_at_imp_Lim_at_within assms(1) continuous_at by blast+
  
  have ?thesis when "c>0" "f x>0"  
  proof -    
    have "(g has_sgnx - sgn (f x)) (at_left x)" 
      using has_sgnx_derivative_at_left[OF g_deriv ‹g x=0›] that by auto
    moreover have "(g has_sgnx sgn (f x)) (at_right x)" 
      using has_sgnx_derivative_at_right[OF g_deriv ‹g x=0›] that by auto
    ultimately have "(LIM t at_left x. f t / g t :> at_bot) ∧ (LIM t at_right x. f t / g t :> at_top)"
      using filterlim_divide_at_bot_at_top_iff[OF _ ‹f x≠0›, of f] 
      using f_tendsto(1) f_tendsto(2) g_tendsto(1) g_tendsto(2) by blast
    moreover have "sgn c = sgn (f x)" using that by auto
    ultimately show ?thesis unfolding jump_def by auto
  qed
  moreover have ?thesis when "c>0" "f x<0"  
  proof -    
    have "(g has_sgnx sgn (f x)) (at_left x)" 
      using has_sgnx_derivative_at_left[OF g_deriv ‹g x=0›] that by auto
    moreover have "(g has_sgnx - sgn (f x)) (at_right x)" 
      using has_sgnx_derivative_at_right[OF g_deriv ‹g x=0›] that by auto
    ultimately have "(LIM t at_left x. f t / g t :> at_top) ∧ (LIM t at_right x. f t / g t :> at_bot)"
      using filterlim_divide_at_bot_at_top_iff[OF _ ‹f x≠0›, of f] 
      using f_tendsto(1) f_tendsto(2) g_tendsto(1) g_tendsto(2) by blast
    moreover from this have "¬ (LIM t at_left x. f t / g t :> at_bot)"
      using filterlim_at_top_at_bot by fastforce
    moreover have "sgn c ≠ sgn (f x)" using that by auto
    ultimately show ?thesis unfolding jump_def by auto
  qed
  moreover have ?thesis when "c<0" "f x>0"  
  proof -    
    have "(g has_sgnx sgn (f x)) (at_left x)" 
      using has_sgnx_derivative_at_left[OF g_deriv ‹g x=0›] that by auto
    moreover have "(g has_sgnx - sgn (f x)) (at_right x)" 
      using has_sgnx_derivative_at_right[OF g_deriv ‹g x=0›] that by auto
    ultimately have "(LIM t at_left x. f t / g t :> at_top) ∧ (LIM t at_right x. f t / g t :> at_bot)"
      using filterlim_divide_at_bot_at_top_iff[OF _ ‹f x≠0›, of f] 
      using f_tendsto(1) f_tendsto(2) g_tendsto(1) g_tendsto(2) by blast
    moreover from this have "¬ (LIM t at_left x. f t / g t :> at_bot)"
      using filterlim_at_top_at_bot by fastforce
    moreover have "sgn c ≠ sgn (f x)" using that by auto
    ultimately show ?thesis unfolding jump_def by auto
  qed
  moreover have ?thesis when "c<0" "f x<0"  
  proof -    
    have "(g has_sgnx - sgn (f x)) (at_left x)" 
      using has_sgnx_derivative_at_left[OF g_deriv ‹g x=0›] that by auto
    moreover have "(g has_sgnx sgn (f x)) (at_right x)" 
      using has_sgnx_derivative_at_right[OF g_deriv ‹g x=0›] that by auto
    ultimately have "(LIM t at_left x. f t / g t :> at_bot) ∧ (LIM t at_right x. f t / g t :> at_top)"
      using filterlim_divide_at_bot_at_top_iff[OF _ ‹f x≠0›, of f] 
      using f_tendsto(1) f_tendsto(2) g_tendsto(1) g_tendsto(2) by blast
    moreover have "sgn c =sgn (f x)" using that by auto
    ultimately show ?thesis unfolding jump_def by auto
  qed
  ultimately show ?thesis using ‹c≠0› ‹f x≠0› by argo   
qed
    
lemma jump_jump_poly: "jump (λx. poly q x / poly p x) a = jump_poly q p a"
proof (cases "p=0")
  case True
  then show ?thesis by auto
next
  case False
  obtain p' q' where p':"p= p'*gcd p q" and q':"q=q'*gcd p q" 
    using gcd_dvd1 gcd_dvd2 dvd_def[of "gcd p q", simplified mult.commute]  by metis
  then have "coprime p' q'" "p'≠0" "gcd p q≠0" using gcd_coprime ‹p≠0›  by auto
  
  define f where "f ≡ (λx. poly q' x / poly p' x)"
  define g where "g ≡ (λx. if poly (gcd p q) x = 0 then 0::real else 1)"
  
  have g_tendsto:"(g ⤏ 1) (at_left a)" "(g ⤏ 1) (at_right a)"
  proof -
    have
      "(poly (gcd p q) has_sgnx 1) (at_left a) 
          ∨ (poly (gcd p q) has_sgnx - 1) (at_left a)"
      "(poly (gcd p q) has_sgnx 1) (at_right a) 
          ∨ (poly (gcd p q) has_sgnx - 1) (at_right a)"
      using ‹p≠0› poly_has_sgnx_values by auto
    then have " ∀F x in at_left a. g x = 1" " ∀F x in at_right a. g x = 1"
      unfolding has_sgnx_def g_def by (auto elim:eventually_mono)
    then show "(g ⤏ 1) (at_left a)" "(g ⤏ 1) (at_right a)"
      using tendsto_eventually by auto
  qed
    
  have "poly q x / poly p x = g x * f x" for x
    unfolding f_def g_def by (subst p',subst q',auto)
  then have "jump (λx. poly q x / poly p x) a = jump (λx. g x * f x) a"
    by auto
  also have "... = jump f a"
    unfolding jump_def
    apply (subst (1 2) filterlim_tendsto_pos_mult_at_top_iff)
        prefer 5
        apply (subst (1 2) filterlim_tendsto_pos_mult_at_bot_iff)
    using g_tendsto by auto
  also have "... = jump_poly q' p' a"
    using jump_jump_poly_aux[OF ‹p'≠0› ‹coprime p' q'›] unfolding f_def by auto
  also have "... = jump_poly q p a"
    using jump_poly_mult[OF ‹gcd p q ≠ 0›, of q'] p' q'
    by (metis mult.commute)
  finally show ?thesis .
qed  
  
 
lemma jump_Im_divide_Re_0:
  assumes "path g" "Re (g x)≠0" "0<x" "x<1"
  shows "jump (λt. Im (g t) / Re (g t)) x = 0"  
proof -
  have "isCont g x"
    using ‹path g›[unfolded path_def] ‹0<x› ‹x<1›
    apply (elim continuous_on_interior)
    by auto
  then have "isCont (λt. Im(g t)/Re(g t)) x" using ‹Re (g x)≠0›  
    by (auto intro:continuous_intros isCont_Re isCont_Im)
  then show "jump (λt. Im(g t)/Re(g t)) x=0"
    using jump_not_infinity by auto 
qed 
  
lemma jumpF_im_divide_Re_0:
  assumes "path g" "Re (g x)≠0" 
  shows "⟦0≤x;x<1⟧ ⟹ jumpF (λt. Im (g t) / Re (g t)) (at_right x) = 0"
        "⟦0<x;x≤1⟧ ⟹ jumpF (λt. Im (g t) / Re (g t)) (at_left x) = 0"
proof -
  define g' where "g' = (λt. Im (g t) / Re (g t))"

  show "jumpF g' (at_right x) = 0" when "0≤x" "x<1"
  proof -
    have "(g' ⤏ g' x) (at_right x)"
    proof (cases "x=0")
      case True
      have "continuous (at_right 0) g" 
        using ‹path g› unfolding path_def 
        by (auto elim:continuous_on_at_right)
      then have "continuous (at_right x) (λt. Im(g t))" "continuous (at_right x) (λt. Re(g t))"
        using continuous_Im continuous_Re True by auto
      moreover have "Re (g (netlimit (at_right x))) ≠ 0" 
        using assms(2) by (simp add: Lim_ident_at)
      ultimately have "continuous (at_right x) (λt. Im (g t)/Re(g t))"  
        by (auto intro:continuous_divide)
      then show ?thesis unfolding g'_def continuous_def 
        by (simp add: Lim_ident_at)
    next
      case False
      have "isCont (λx. Im (g x)) x" "isCont (λx. Re (g x)) x" 
        using ‹path g› unfolding path_def
        by (metis False atLeastAtMost_iff at_within_Icc_at continuous_Im continuous_Re
          continuous_on_eq_continuous_within less_le that)+      
      then have "isCont g' x" 
        using assms(2) unfolding g'_def
        by (auto intro:continuous_intros)
      then show ?thesis unfolding isCont_def using filterlim_at_split by blast
    qed
    then have "¬ filterlim g' at_top (at_right x)" "¬ filterlim g' at_bot (at_right x)"
      using filterlim_at_top_nhds[of g' "at_right x"] filterlim_at_bot_nhds[of g' "at_right x"]
      by auto
    then show ?thesis unfolding jumpF_def by auto
  qed
    
  show "jumpF g' (at_left x) = 0" when "0<x" "x≤1"
  proof -
    have "(g' ⤏ g' x) (at_left x)"
    proof (cases "x=1")
      case True
      have "continuous (at_left 1) g" 
        using ‹path g› unfolding path_def 
        by (auto elim:continuous_on_at_left)
      then have "continuous (at_left x) (λt. Im(g t))" "continuous (at_left x) (λt. Re(g t))"
        using continuous_Im continuous_Re True by auto
      moreover have "Re (g (netlimit (at_left x))) ≠ 0" 
        using assms(2) by (simp add: Lim_ident_at)
      ultimately have "continuous (at_left x) (λt. Im (g t)/Re(g t))"  
        by (auto intro:continuous_divide)
      then show ?thesis unfolding g'_def continuous_def 
        by (simp add: Lim_ident_at)
    next
      case False
      have "isCont (λx. Im (g x)) x" "isCont (λx. Re (g x)) x" 
        using ‹path g› unfolding path_def
        by (metis False atLeastAtMost_iff at_within_Icc_at continuous_Im continuous_Re
          continuous_on_eq_continuous_within less_le that)+      
      then have "isCont g' x" 
        using assms(2) unfolding g'_def
        by (auto)
      then show ?thesis unfolding isCont_def using filterlim_at_split by blast
    qed
    then have "¬ filterlim g' at_top (at_left x)" "¬ filterlim g' at_bot (at_left x)"
      using filterlim_at_top_nhds[of g' "at_left x"] filterlim_at_bot_nhds[of g' "at_left x"]
      by auto
    then show ?thesis unfolding jumpF_def by auto
  qed 
qed
  
lemma jump_cong:
  assumes "x=y" and "eventually (λx. f x=g x) (at x)"
  shows "jump f x = jump g y"
proof -
  have left:"eventually (λx. f x=g x) (at_left x)" 
    and right:"eventually (λx. f x=g x) (at_right x)"
    using assms(2) eventually_at_split by blast+
  from filterlim_cong[OF _ _ this(1)] filterlim_cong[OF _ _ this(2)] 
  show ?thesis unfolding jump_def using assms(1) by fastforce
qed 
    
lemma jumpF_cong:
  assumes "F=G" and "eventually (λx. f x=g x) F"
  shows "jumpF f F = jumpF g G"
proof -
  have "∀F r in G. f r = g r"
    using assms(1) assms(2) by force
  then show ?thesis
    by (simp add: assms(1) filterlim_cong jumpF_def)
qed
  
lemma jump_at_left_at_right_eq:
  assumes "isCont f x" and "f x ≠ 0" and sgnx_eq:"sgnx g (at_left x) = sgnx g (at_right x)"
  shows "jump (λt. f t/g t) x = 0"  
proof -
  define c where "c = sgn (f x)"
  then have "c≠0" using ‹f x≠0› by (simp add: sgn_zero_iff)
  have f_tendsto:"(f ⤏ f x) (at_left x)" " (f ⤏ f x) (at_right x)"
    using ‹isCont f x› Lim_at_imp_Lim_at_within isCont_def by blast+
  have False when "(g has_sgnx - c) (at_left x)" "(g has_sgnx c) (at_right x)" 
  proof -
    have "sgnx g (at_left x) = -c" using that(1) by auto
    moreover have "sgnx g (at_right x) = c" using that(2) by auto
    ultimately show False using sgnx_eq ‹c≠0› by force
  qed
  moreover have False when "(g has_sgnx c) (at_left x)" "(g has_sgnx - c) (at_right x)" 
  proof -
    have "sgnx g (at_left x) = c" using that(1) by auto
    moreover have "sgnx g (at_right x) = - c" using that(2) by auto
    ultimately show False using sgnx_eq ‹c≠0› by force
  qed  
  ultimately show ?thesis
    unfolding jump_def
    by (auto simp add:f_tendsto filterlim_divide_at_bot_at_top_iff[OF _ ‹f x ≠ 0›] c_def)  
qed  
  
lemma jumpF_pos_has_sgnx:
  assumes "jumpF f F > 0"
  shows "(f has_sgnx 1) F"
proof -
  have "filterlim f at_top F" using assms unfolding jumpF_def by argo
  then have "eventually (λx. f x>0) F" using filterlim_at_top_dense[of f F] by blast
  then show ?thesis unfolding has_sgnx_def 
    apply (elim eventually_mono)
    by auto
qed  

lemma jumpF_neg_has_sgnx:
  assumes "jumpF f F < 0"
  shows "(f has_sgnx -1) F"
proof -
  have "filterlim f at_bot F" using assms unfolding jumpF_def by argo
  then have "eventually (λx. f x<0) F" using filterlim_at_bot_dense[of f F] by blast
  then show ?thesis unfolding has_sgnx_def 
    apply (elim eventually_mono)
    by auto
qed

  
lemma jumpF_IVT:
  fixes f::"real ⇒ real" and a b::real
  defines "right≡(λ(R::real ⇒ real ⇒ bool). R (jumpF f (at_right a)) 0 
                      ∨ (continuous (at_right a) f ∧ R (f a) 0))"
    and
          "left≡(λ(R::real ⇒ real ⇒ bool). R (jumpF f (at_left b)) 0 
                      ∨ (continuous (at_left b) f ∧ R (f b) 0))"
  assumes "a<b" and cont:"continuous_on {a<..<b} f" and
    right_left:"right greater ∧ left less ∨ right less ∧ left greater" 
  shows "∃x. a<x ∧ x<b ∧ f x =0"
proof -
  have ?thesis when "right greater" "left less" 
  proof -
    have "(f has_sgnx 1) (at_right a)"
    proof -
      have ?thesis when "jumpF f (at_right a)>0" using jumpF_pos_has_sgnx[OF that] .
      moreover have ?thesis when "f a > 0" "continuous (at_right a) f"
      proof -
        have "(f ⤏ f a) (at_right a)" using that(2) by (simp add: continuous_within)
        then show ?thesis
          using tendsto_nonzero_has_sgnx[of f "f a" "at_right a"] that by auto
      qed
      ultimately show ?thesis using that(1) unfolding right_def by auto
    qed
    then obtain a' where "a<a'" and a'_def:"∀y. a<y ∧ y < a' ⟶ f y > 0" 
      unfolding has_sgnx_def eventually_at_right using sgn_1_pos by auto
    have "(f has_sgnx - 1) (at_left b)" 
    proof -
      have ?thesis when "jumpF f (at_left b)<0" using jumpF_neg_has_sgnx[OF that] .
      moreover have ?thesis when "f b < 0" "continuous (at_left b) f" 
      proof -
        have "(f ⤏ f b) (at_left b)" 
          using that(2) by (simp add: continuous_within)
        then show ?thesis
          using tendsto_nonzero_has_sgnx[of f "f b" "at_left b"] that by auto
      qed
      ultimately show ?thesis using that(2) unfolding left_def by auto
    qed
    then obtain b' where "b'<b" and b'_def:"∀y. b'<y ∧ y < b ⟶ f y < 0" 
      unfolding has_sgnx_def eventually_at_left using sgn_1_neg by auto  
    have "a' ≤ b'"
    proof (rule ccontr)
      assume "¬ a' ≤ b'"
      then have "{a<..<a'} ∩ {b'<..<b} ≠ {}"
        using ‹a<a'› ‹b'<b› ‹a<b› by auto
      then obtain c where "c∈{a<..<a'}" "c∈{b'<..<b}" by blast
      then have "f c>0" "f c<0"
        using a'_def b'_def by auto
      then show False by auto
    qed
    define a0 where "a0=(a+a')/2"
    define b0 where "b0=(b+b')/2"
    have [simp]:"a<a0" "a0<a'" "a0<b0" "b'<b0" "b0<b" 
      unfolding a0_def b0_def using ‹a<a'› ‹b'<b› ‹a'≤b'› by auto   
    have "f a0>0" "f b0<0" using a'_def[rule_format,of a0] b'_def[rule_format,of b0] by auto
    moreover have "continuous_on {a0..b0} f"
      using cont ‹a < a0› ‹b0 < b›
      by (meson atLeastAtMost_subseteq_greaterThanLessThan_iff continuous_on_subset)
    ultimately have "∃x>a0. x < b0 ∧ f x = 0"
      using IVT_strict[of 0 f a0 b0] by auto
    then show ?thesis using ‹a < a0› ‹b0 < b› 
      by (meson lessThan_strict_subset_iff psubsetE subset_psubset_trans)
  qed
  moreover have ?thesis when "right less" "left greater" 
  proof -
    have "(f has_sgnx -1) (at_right a)"
    proof -
      have ?thesis when "jumpF f (at_right a)<0" using jumpF_neg_has_sgnx[OF that] .
      moreover have ?thesis when "f a < 0" "continuous (at_right a) f"
      proof -
        have "(f ⤏ f a) (at_right a)" 
          using that(2) by (simp add: continuous_within)
        then show ?thesis
          using tendsto_nonzero_has_sgnx[of f "f a" "at_right a"] that by auto
      qed
      ultimately show ?thesis using that(1) unfolding right_def by auto
    qed
    then obtain a' where "a<a'" and a'_def:"∀y. a<y ∧ y < a' ⟶ f y < 0" 
      unfolding has_sgnx_def eventually_at_right using sgn_1_neg by auto
    have "(f has_sgnx  1) (at_left b)" 
    proof -
      have ?thesis when "jumpF f (at_left b)>0" using jumpF_pos_has_sgnx[OF that] .
      moreover have ?thesis when "f b > 0" "continuous (at_left b) f"
      proof -
        have "(f ⤏ f b) (at_left b)" 
          using that(2) by (simp add: continuous_within)
        then show ?thesis
          using tendsto_nonzero_has_sgnx[of f "f b" "at_left b"] that by auto
      qed
      ultimately show ?thesis using that(2) unfolding left_def by auto
    qed
    then obtain b' where "b'<b" and b'_def:"∀y. b'<y ∧ y < b ⟶ f y > 0" 
      unfolding has_sgnx_def eventually_at_left using sgn_1_pos by auto  
    have "a' ≤ b'"
    proof (rule ccontr)
      assume "¬ a' ≤ b'"
      then have "{a<..<a'} ∩ {b'<..<b} ≠ {}"
        using ‹a<a'› ‹b'<b› ‹a<b› by auto
      then obtain c where "c∈{a<..<a'}" "c∈{b'<..<b}" by blast
      then have "f c>0" "f c<0"
        using a'_def b'_def by auto
      then show False by auto
    qed
    define a0 where "a0=(a+a')/2"
    define b0 where "b0=(b+b')/2"
    have [simp]:"a<a0" "a0<a'" "a0<b0" "b'<b0" "b0<b" 
      unfolding a0_def b0_def using ‹a<a'› ‹b'<b› ‹a'≤b'› by auto   
    have "f a0<0" "f b0>0" using a'_def[rule_format,of a0] b'_def[rule_format,of b0] by auto
    moreover have "continuous_on {a0..b0} f"
      using cont  ‹a < a0› ‹b0 < b› 
      by (meson atLeastAtMost_subseteq_greaterThanLessThan_iff continuous_on_subset)  
    ultimately have "∃x>a0. x < b0 ∧ f x = 0"
      using IVT_strict[of 0 f a0 b0] by auto
    then show ?thesis using ‹a < a0› ‹b0 < b› 
      by (meson lessThan_strict_subset_iff psubsetE subset_psubset_trans)
  qed  
  ultimately show ?thesis using right_left by auto
qed
   
lemma jumpF_eventually_const:
  assumes "eventually (λx. f x=c) F" "F≠bot"
  shows "jumpF f F = 0"
proof -
  have "jumpF f F = jumpF (λ_. c) F"
    apply (rule jumpF_cong)
    using assms(1) by auto
  also have "... = 0" using jumpF_const[OF ‹F≠bot›] by simp
  finally show ?thesis .
qed

lemma jumpF_tan_comp:
  "jumpF (f o tan) (at_right x) = (if cos x = 0 
      then jumpF f at_bot else jumpF f (at_right (tan x)))"
  "jumpF (f o tan) (at_left x) = (if cos x =0 
      then jumpF f at_top else jumpF f (at_left (tan x)))"
proof -
  have "filtermap (f ∘ tan) (at_right x) = 
      (if cos x = 0 then filtermap f at_bot else filtermap f (at_right (tan x)))"
    unfolding comp_def
    apply (subst filtermap_filtermap[of f tan,symmetric])
    using filtermap_tan_at_right_inf filtermap_tan_at_right by auto
  then show "jumpF (f o tan) (at_right x) = (if cos x = 0 
          then jumpF f at_bot else jumpF f (at_right (tan x)))"
    unfolding jumpF_def filterlim_def by auto
next
  have "filtermap (f ∘ tan) (at_left x) = 
      (if cos x = 0 then filtermap f at_top else filtermap f (at_left (tan x)))"
    unfolding comp_def
    apply (subst filtermap_filtermap[of f tan,symmetric])
    using filtermap_tan_at_left_inf filtermap_tan_at_left by auto
  then show "jumpF (f o tan) (at_left x) = (if cos x = 0 
          then jumpF f at_top else jumpF f (at_left (tan x)))"
    unfolding jumpF_def filterlim_def by auto
qed

subsection ‹Finite jumpFs over an interval›

definition finite_jumpFs::"(real ⇒ real) ⇒ real ⇒ real ⇒  bool" where
  "finite_jumpFs f a b = finite {x. (jumpF f (at_left x) ≠0 ∨ jumpF f (at_right x) ≠0) ∧ a≤x ∧ x≤b}" 
  
lemma finite_jumpFs_linear_pos:
  assumes "c>0"
  shows "finite_jumpFs (f o (λx. c * x + b)) lb ub ⟷ finite_jumpFs f (c * lb +b) (c * ub + b)" 
proof -
  define left where "left = (λf lb ub. {x. jumpF f (at_left x) ≠ 0 ∧ lb ≤ x ∧ x ≤ ub})"
  define right where "right = (λf lb ub. {x. jumpF f (at_right x) ≠ 0 ∧ lb ≤ x ∧ x ≤ ub})"
  define g where "g=(λx. c*x+b)"
  define gi where "gi = (λx. (x-b)/c)"
  have "finite_jumpFs (f o (λx. c * x + b)) lb ub 
      = finite (left (f o g) lb ub ∪ right (f o g) lb ub)"
    unfolding finite_jumpFs_def  
    apply (rule arg_cong[where f=finite]) 
    by (auto simp add:left_def right_def g_def)
  also have "... = finite (gi ` (left f (g lb) (g ub) ∪ right f (g lb) (g ub)))"
  proof -
    have j_rw:
      "jumpF (f o g) (at_left x) = jumpF f (at_left (g x))" 
      "jumpF (f o g) (at_right x) = jumpF f (at_right (g x))"
        for x 
      using jumpF_linear_comp[of c f b x] ‹c>0› unfolding g_def by auto
    then have 
        "left (f o g) lb ub = gi ` left f (g lb) (g ub)"
        "right (f o g) lb ub = gi ` right f (g lb) (g ub)"
      unfolding left_def right_def gi_def
      using ‹c>0› by (auto simp add:g_def field_simps) 
    then have "left (f o g) lb ub ∪ right (f o g) lb ub 
        = gi ` (left f (g lb) (g ub) ∪ right f (g lb) (g ub))"
      by auto
    then show ?thesis by auto
  qed
  also have "... = finite (left f (g lb) (g ub) ∪ right f (g lb) (g ub))"
    apply (rule finite_image_iff)
    unfolding gi_def using ‹c >0›  inj_on_def by fastforce
  also have "... =  finite_jumpFs f (c * lb +b) (c * ub + b)"   
    unfolding finite_jumpFs_def
    apply (rule arg_cong[where f=finite]) 
    by (auto simp add:left_def right_def g_def)
  finally show ?thesis .
qed
  
lemma finite_jumpFs_consts:
  "finite_jumpFs (λ_ . c) lb ub"
  unfolding finite_jumpFs_def using jumpF_const by auto
    
lemma finite_jumpFs_combine:
  assumes "finite_jumpFs f a b" "finite_jumpFs f b c" 
  shows "finite_jumpFs f a c"
proof -
  define P where "P=(λx. jumpF f (at_left x) ≠ 0 ∨ jumpF f (at_right x) ≠ 0)"
  have "{x. P x ∧ a ≤ x ∧ x ≤ c} ⊆ {x. P x ∧ a ≤ x ∧ x≤b} ∪ {x. P x ∧ b ≤x ∧ x≤c}"
    by auto
  moreover have "finite ({x. P x ∧ a ≤ x ∧ x≤b} ∪ {x. P x ∧ b ≤x ∧ x≤c})"
    using assms unfolding finite_jumpFs_def P_def by auto
  ultimately have "finite {x. P x ∧ a ≤ x ∧ x ≤ c}" 
    using finite_subset by auto    
  then show ?thesis unfolding finite_jumpFs_def P_def by auto
qed
    
lemma finite_jumpFs_subE:
  assumes "finite_jumpFs f a b" "a≤a'" "b'≤b" 
  shows "finite_jumpFs f a' b'"  
using assms unfolding finite_jumpFs_def
  apply (elim rev_finite_subset)
  by auto
   
lemma finite_Psegments_Re_imp_jumpFs:
  assumes "finite_Psegments (λt. Re (g t - z) = 0) a b" "continuous_on {a..b} g" 
  shows "finite_jumpFs (λt. Im (g t - z)/Re (g t - z)) a b"
    using assms
proof (induct rule:finite_Psegments.induct)
  case (emptyI a b) 
  then show ?case unfolding finite_jumpFs_def 
    by (auto intro:rev_finite_subset[of "{a}"])    
next
  case (insertI_1 s a b)
  define f where "f=(λt. Im (g t - z) / Re (g t - z))"
  have "finite_jumpFs f a s" 
  proof -
    have "continuous_on {a..s} g" using ‹continuous_on {a..b} g› ‹s ∈ {a..<b}› 
      by (auto elim:continuous_on_subset)
    then show ?thesis using insertI_1 unfolding f_def by auto
  qed
  moreover have "finite_jumpFs f s b" 
  proof -
    have "jumpF f (at_left x) =0" "jumpF f (at_right x) = 0" when "x∈{s<..<b}" for x
    proof - 
      show "jumpF f (at_left x) =0"
        apply (rule jumpF_eventually_const[of _ 0])
        unfolding eventually_at_left
         apply (rule exI[where x=s])
        using that insertI_1 unfolding f_def by auto
      show "jumpF f (at_right x) = 0"
        apply (rule jumpF_eventually_const[of _ 0])
        unfolding eventually_at_right
         apply (rule exI[where x=b])
        using that insertI_1 unfolding f_def by auto 
    qed
    then have "{x. (jumpF f (at_left x) ≠ 0 ∨ jumpF f (at_right x) ≠ 0) ∧ s ≤ x ∧ x ≤ b}
          = {x. (jumpF f (at_left x) ≠ 0 ∨ jumpF f (at_right x) ≠ 0) ∧ (x=s ∨ x = b)}"
      using  ‹s∈{a..<b}› by force
    then show ?thesis unfolding finite_jumpFs_def by auto
  qed
  ultimately show ?case using finite_jumpFs_combine[of _ a s b] unfolding f_def by auto
next
  case (insertI_2 s a b)
  define f where "f=(λt. Im (g t - z) / Re (g t - z))"
  have "finite_jumpFs f a s" 
  proof -
    have "continuous_on {a..s} g" using ‹continuous_on {a..b} g› ‹s ∈ {a..<b}› 
      by (auto elim:continuous_on_subset)
    then show ?thesis using insertI_2 unfolding f_def by auto
  qed
  moreover have "finite_jumpFs f s b" 
  proof -
    have "jumpF f (at_left x) =0" "jumpF f (at_right x) = 0" when "x∈{s<..<b}" for x
    proof - 
      have "isCont f x" 
        unfolding f_def
        apply (intro continuous_intros isCont_Im isCont_Re 
            continuous_on_interior[OF ‹continuous_on {a..b} g›])
        using insertI_2.hyps(1) that 
          apply auto[2]
        using insertI_2.hyps(3) that by blast
      then show "jumpF f (at_left x) =0" "jumpF f (at_right x) = 0"
        by (simp_all add: continuous_at_split jumpF_not_infinity)
    qed
    then have "{x. (jumpF f (at_left x) ≠ 0 ∨ jumpF f (at_right x) ≠ 0) ∧ s ≤ x ∧ x ≤ b}
          = {x. (jumpF f (at_left x) ≠ 0 ∨ jumpF f (at_right x) ≠ 0) ∧ (x=s ∨ x = b)}"
      using  ‹s∈{a..<b}› by force
    then show ?thesis unfolding finite_jumpFs_def by auto
  qed
  ultimately show ?case using finite_jumpFs_combine[of _ a s b] unfolding f_def by auto
qed
  
lemma finite_ReZ_segments_imp_jumpFs:
  assumes "finite_ReZ_segments g z" "path g" 
  shows "finite_jumpFs (λt. Im (g t - z)/Re (g t - z)) 0 1"
  using assms unfolding finite_ReZ_segments_def path_def
  by (rule finite_Psegments_Re_imp_jumpFs)      
    
subsection ‹@{term jumpF} at path ends›  

definition jumpF_pathstart::"(real ⇒ complex) ⇒ complex ⇒ real" where
  "jumpF_pathstart g z= jumpF (λt. Im(g t- z)/Re(g t - z)) (at_right 0)"
 
definition jumpF_pathfinish::"(real ⇒ complex) ⇒ complex ⇒ real" where
  "jumpF_pathfinish g z= jumpF (λt. Im(g t - z)/Re(g t -z)) (at_left 1)"
  
lemma jumpF_pathstart_eq_0:
  assumes "path g" "Re(pathstart g)≠Re z"
  shows "jumpF_pathstart g z = 0"
unfolding jumpF_pathstart_def 
  apply (rule jumpF_im_divide_Re_0)
  using assms[unfolded pathstart_def] by auto

lemma jumpF_pathfinish_eq_0:
  assumes "path g" "Re(pathfinish g)≠Re z"
  shows "jumpF_pathfinish g z = 0"
unfolding jumpF_pathfinish_def 
  apply (rule jumpF_im_divide_Re_0)
  using assms[unfolded pathfinish_def] by auto  
   
lemma 
  shows jumpF_pathfinish_reversepath: "jumpF_pathfinish (reversepath g) z = jumpF_pathstart g z"
    and jumpF_pathstart_reversepath: "jumpF_pathstart (reversepath g) z = jumpF_pathfinish g z"
proof -
  define f where "f=(λt. Im (g t - z) / Re (g t - z))"
  define f' where "f'=(λt. Im (reversepath g t - z) / Re (reversepath g t - z))"
  have "f o (λt. 1 - t) = f'"
    unfolding f_def f'_def comp_def reversepath_def by auto
  then show "jumpF_pathfinish (reversepath g) z = jumpF_pathstart g z" 
        "jumpF_pathstart (reversepath g) z = jumpF_pathfinish g z" 
    unfolding jumpF_pathstart_def jumpF_pathfinish_def
    using jumpF_linear_comp(2)[of "-1" f 1 0,simplified] jumpF_linear_comp(1)[of "-1" f 1 1,simplified]
    apply (fold f_def f'_def)    
    by auto
qed
     
lemma jumpF_pathstart_joinpaths[simp]:
  "jumpF_pathstart (g1+++g2) z = jumpF_pathstart g1 z"
proof -
  let ?h="(λt. Im (g1 t - z) / Re (g1 t - z))"
  let ?f="λt. Im ((g1 +++ g2) t - z) / Re ((g1 +++ g2) t - z)"
  have "jumpF_pathstart g1 z = jumpF ?h (at_right 0)"
    unfolding jumpF_pathstart_def by simp
  also have "... = jumpF (?h o (λt. 2*t)) (at_right 0)"
    using jumpF_linear_comp[of 2 ?h 0 0,simplified] by auto
  also have "... = jumpF ?f (at_right 0)"
  proof (rule jumpF_cong)
    show " ∀F x in at_right 0. (?h ∘ (*) 2) x =?f x"
      unfolding eventually_at_right
      apply (intro exI[where x="1/2"])
      by (auto simp add:joinpaths_def)
  qed simp
  also have "... =jumpF_pathstart (g1+++g2) z"
    unfolding jumpF_pathstart_def by simp
  finally show ?thesis by simp
qed
  
lemma jumpF_pathfinish_joinpaths[simp]:
  "jumpF_pathfinish (g1+++g2) z = jumpF_pathfinish g2 z"
proof -
  let ?h="(λt. Im (g2 t - z) / Re (g2 t - z))"
  let ?f="λt. Im ((g1 +++ g2) t - z) / Re ((g1 +++ g2) t - z)"
  have "jumpF_pathfinish g2 z = jumpF ?h (at_left 1)"
    unfolding jumpF_pathfinish_def by simp
  also have "... = jumpF (?h o (λt. 2*t-1)) (at_left 1)"
    using jumpF_linear_comp[of 2 _ "-1" 1,simplified] by auto
  also have "... = jumpF ?f (at_left 1)"
  proof (rule jumpF_cong)
    show " ∀F x in at_left 1. (?h ∘ (λt. 2 * t - 1)) x =?f x"
      unfolding eventually_at_left
      apply (intro exI[where x="1/2"])
      by (auto simp add:joinpaths_def)
  qed simp
  also have "... =jumpF_pathfinish (g1+++g2) z"
    unfolding jumpF_pathfinish_def by simp
  finally show ?thesis by simp
qed  
  
subsection ‹Cauchy index›  

―‹Deprecated, use "cindexE" if possible›
definition cindex::"real ⇒ real ⇒ (real ⇒ real) ⇒ int" where
  "cindex a b f = (∑x∈{x. jump f x≠0 ∧ a<x ∧ x<b}. jump f x )"

definition cindexE::"real ⇒ real ⇒ (real ⇒ real) ⇒ real" where
  "cindexE a b f = (∑x∈{x. jumpF f (at_right x) ≠0 ∧ a≤x ∧ x<b}. jumpF f (at_right x)) 
                    - (∑x∈{x. jumpF f (at_left x) ≠0 ∧ a<x ∧ x≤b}. jumpF f (at_left x))"     

definition cindexE_ubd::"(real ⇒ real) ⇒ real" where
  "cindexE_ubd f = (∑x∈{x. jumpF f (at_right x) ≠0 }. jumpF f (at_right x)) 
                      - (∑x∈{x. jumpF f (at_left x) ≠0}. jumpF f (at_left x))"

  
lemma cindexE_empty:
  "cindexE a a f = 0"
  unfolding cindexE_def by (simp add: sum.neutral)     
  
lemma cindex_const: "cindex a b (λ_. c) = 0"
  unfolding cindex_def
  apply (rule sum.neutral)
  by auto
      
lemma cindex_eq_cindex_poly: "cindex a b (λx. poly q x/poly p x) = cindex_poly a b q p"  
proof (cases "p=0")
  case True
  then show ?thesis using cindex_const by auto
next
  case False
  have "cindex_poly a b q p = 
      (∑x |jump_poly q p x ≠0 ∧ a < x ∧ x < b. jump_poly q p x)"
    unfolding cindex_poly_def 
    apply (rule sum.mono_neutral_cong_right)
    using jump_poly_not_root by (auto simp add: ‹p≠0› poly_roots_finite)
  also have "... = cindex a b (λx. poly q x/poly p x)"
    unfolding cindex_def
    apply (rule sum.cong)
    using jump_jump_poly[of q] by auto
  finally show ?thesis by auto
qed
  
lemma cindex_combine:
  assumes finite:"finite {x. jump f x≠0 ∧ a<x ∧ x<c}" and "a<b" "b<c"
  shows "cindex a c f = cindex a b f  + jump f b + cindex b c f"
proof -
  define ssum where "ssum = (λs. sum (jump f) ({x. jump f x≠0 ∧ a<x ∧ x<c} ∩ s))"  
  have ssum_union:"ssum (A ∪ B) = ssum A + ssum B" when "A ∩ B ={}" for A B
  proof -
    define C where "C={x. jump f x ≠ 0 ∧ a<x ∧ x<c}"
    have "finite C" using finite unfolding C_def .
    then show ?thesis
      unfolding ssum_def
      apply (fold C_def)
      using sum_Un[of "C ∩ A" "C ∩ B"] that
      by (simp add: inf_assoc inf_sup_aci(3) inf_sup_distrib1 sum.union_disjoint)
  qed
  have "cindex a c f = ssum ({a<..<b} ∪ {b} ∪ {b<..<c})"
    unfolding ssum_def cindex_def 
    apply (rule sum.cong[of _ _ "jump f" "jump f",simplified])
    using ‹a<b› ‹b<c› by fastforce
  moreover have "cindex a b f = ssum {a<..<b}" 
    unfolding cindex_def ssum_def using ‹a<b› ‹b<c› 
    by (intro sum.cong,auto)
  moreover have "jump f b = ssum {b}" 
    unfolding ssum_def using ‹a<b› ‹b<c›  by (cases "jump f b=0",auto)
  moreover have "cindex b c f = ssum {b<..<c}" 
    unfolding cindex_def ssum_def using ‹a<b› ‹b<c›  by (intro sum.cong,auto)
  ultimately show ?thesis 
    apply (subst (asm) ssum_union,simp)
    by (subst (asm) ssum_union,auto)
qed
 
lemma cindexE_combine:
  assumes finite:"finite_jumpFs f a c" and "a≤b" "b≤c"
  shows "cindexE a c f = cindexE a b f + cindexE b c f" 
proof -
  define S where "S={x. (jumpF f (at_left x) ≠ 0 ∨ jumpF f (at_right x) ≠ 0) ∧ a ≤ x ∧ x ≤ c}"
  define A0 where "A0={x. jumpF f (at_right x) ≠ 0 ∧ a ≤ x ∧ x < c}"
  define A1 where "A1={x. jumpF f (at_right x) ≠ 0 ∧ a ≤ x ∧ x < b}" 
  define A2 where "A2={x. jumpF f (at_right x) ≠ 0 ∧ b ≤ x ∧ x < c}"
  define B0 where "B0={x. jumpF f (at_left x) ≠ 0 ∧ a < x ∧ x ≤ c}"
  define B1 where "B1={x. jumpF f (at_left x) ≠ 0 ∧ a < x ∧ x ≤ b}" 
  define B2 where "B2={x. jumpF f (at_left x) ≠ 0 ∧ b < x ∧ x ≤ c}"
  have [simp]:"finite A1" "finite A2" "finite B1" "finite B2" 
  proof -
    have "finite S" using finite unfolding finite_jumpFs_def S_def by auto
    moreover have "A1 ⊆ S" "A2 ⊆ S" "B1 ⊆ S" "B2 ⊆ S"
      unfolding A1_def A2_def B1_def B2_def S_def using ‹a≤b› ‹b≤c› by auto
    ultimately show "finite A1" "finite A2" "finite B1" "finite B2" by (auto elim:finite_subset)
  qed 
  have "cindexE a c f = sum (λx. jumpF f (at_right x)) A0 
        - sum (λx. jumpF f (at_left x)) B0"
    unfolding cindexE_def A0_def B0_def by auto
  also have "... = sum (λx. jumpF f (at_right x)) (A1 ∪ A2) 
        - sum (λx. jumpF f (at_left x)) (B1 ∪ B2)"
  proof -
    have "A0=A1∪A2" unfolding A0_def A1_def A2_def using assms by auto
    moreover have "B0=B1∪B2" unfolding B0_def B1_def B2_def using assms by auto
    ultimately show ?thesis by auto
  qed
  also have "... = cindexE a b f + cindexE b c f"
  proof -
    have "A1 ∩ A2 = {}" unfolding A1_def A2_def by auto
    moreover have "B1 ∩ B2 = {}" unfolding B1_def B2_def by auto
    ultimately show ?thesis
      unfolding cindexE_def  
      apply (fold A1_def A2_def B1_def B2_def)
      by (auto simp add:sum.union_disjoint) 
  qed
  finally show ?thesis .
qed

lemma cindex_linear_comp:
  assumes "c≠0"
  shows "cindex lb ub (f o (λx. c*x+b)) = (if c>0 
    then cindex (c*lb+b) (c*ub+b) f 
    else - cindex (c*ub+b) (c*lb+b) f)"
proof (cases "c>0")
  case False
  then have "c<0" using ‹c≠0› by auto
  have "cindex lb ub (f o (λx. c*x+b)) = - cindex (c*ub+b) (c*lb+b) f"
    unfolding cindex_def
    apply (subst sum_negf[symmetric])
    apply (intro sum.reindex_cong[of "λx. (x-b)/c"])
    subgoal by (simp add: inj_on_def)
    subgoal using False
      apply (subst jump_linear_comp[OF ‹c≠0›])
      by (auto simp add:‹c<0› ‹c≠0› field_simps)
    subgoal for x
      apply (subst jump_linear_comp[OF ‹c≠0›])
      by (auto simp add:‹c<0› ‹c≠0› False field_simps)
    done 
  then show ?thesis using False by auto
next
  case True
  have "cindex lb ub (f o (λx. c*x+b)) = cindex (c*lb+b) (c*ub+b) f"
    unfolding cindex_def
    apply (intro sum.reindex_cong[of "λx. (x-b)/c"])
    subgoal by (simp add: inj_on_def)
    subgoal 
      apply (subst jump_linear_comp[OF ‹c≠0›])
      by (auto simp add: True ‹c≠0› field_simps)
    subgoal for x
      apply (subst jump_linear_comp[OF ‹c≠0›])
      by (auto simp add: ‹c≠0› True field_simps)
    done 
  then show ?thesis using True by auto
qed     

lemma cindexE_linear_comp: 
  assumes "c≠0"
  shows "cindexE lb ub (f o (λx. c*x+b)) = (if c>0 
    then cindexE (c*lb+b) (c*ub+b) f 
    else - cindexE (c*ub+b) (c*lb+b) f)"  
proof -
  define cright where "cright = (λlb ub f. (∑x | jumpF f (at_right x) ≠ 0 ∧ lb ≤ x ∧ x < ub. 
                        jumpF f (at_right x)))"
  define cleft where "cleft = (λlb ub f. (∑x | jumpF f (at_left x) ≠ 0 ∧ lb < x ∧ x ≤ ub. 
                        jumpF f (at_left x)))"
  have cindexE_unfold:"cindexE lb ub f = cright lb ub f - cleft lb ub f"
    for lb ub f unfolding cindexE_def cright_def cleft_def by auto
  have ?thesis when "c<0"
  proof -
    have "cright lb ub (f ∘ (λx. c * x + b)) = cleft (c * ub + b) (c * lb + b) f" 
      unfolding cright_def cleft_def
      apply (intro sum.reindex_cong[of "λx. (x-b)/c"])
      subgoal by (simp add: inj_on_def)
      subgoal using that
        by (subst jumpF_linear_comp[OF ‹c≠0›],auto simp add:field_simps)
      subgoal for x using that
        by (subst jumpF_linear_comp[OF ‹c≠0›],auto simp add: field_simps)
      done  
    moreover have "cleft lb ub (f ∘ (λx. c * x + b)) = cright (c*ub+b) (c*lb + b) f" 
      unfolding cright_def cleft_def
      apply (intro sum.reindex_cong[of "λx. (x-b)/c"])
      subgoal by (simp add: inj_on_def)
      subgoal using that
        by (subst jumpF_linear_comp[OF ‹c≠0›],auto simp add:field_simps)
      subgoal for x using that
        by (subst jumpF_linear_comp[OF ‹c≠0›],auto simp add: field_simps)
      done 
    ultimately show ?thesis unfolding cindexE_unfold using that by auto 
  qed
  moreover have ?thesis when "c>0"
  proof -
    have "cright lb ub (f ∘ (λx. c * x + b)) = cright (c * lb + b) (c * ub + b) f" 
      unfolding cright_def cleft_def
      apply (intro sum.reindex_cong[of "λx. (x-b)/c"])
      subgoal by (simp add: inj_on_def)
      subgoal using that
        by (subst jumpF_linear_comp[OF ‹c≠0›],auto simp add:field_simps)
      subgoal for x using that
        by (subst jumpF_linear_comp[OF ‹c≠0›],auto simp add: field_simps)
      done   
    moreover have "cleft lb ub (f ∘ (λx. c * x + b)) = cleft (c*lb+b) (c*ub + b) f" 
      unfolding cright_def cleft_def
      apply (intro sum.reindex_cong[of "λx. (x-b)/c"])
      subgoal by (simp add: inj_on_def)
      subgoal using that
        by (subst jumpF_linear_comp[OF ‹c≠0›],auto simp add:field_simps)
      subgoal for x using that
        by (subst jumpF_linear_comp[OF ‹c≠0›],auto simp add: field_simps)
      done 
    ultimately show ?thesis unfolding cindexE_unfold using that by auto
  qed
  ultimately show ?thesis using ‹c≠0› by auto
qed

lemma cindexE_cong:
  assumes "finite s" and fg_eq:"⋀x. ⟦a<x;x<b;x∉s⟧ ⟹ f x = g x"
  shows "cindexE a b f = cindexE a b g"
proof -
  define left where 
      "left=(λf. (∑x | jumpF f (at_left x) ≠ 0 ∧ a < x ∧ x ≤ b. jumpF f (at_left x)))"
  define right where 
      "right=(λf. (∑x | jumpF f (at_right x) ≠ 0 ∧ a ≤ x ∧ x < b. jumpF f (at_right x)))"
  have "left f = left g"
  proof -
    have "jumpF f (at_left x) = jumpF g (at_left x)" when "a<x" "x≤b" for x 
    proof (rule jumpF_cong)
      define cs where "cs ≡ {y∈s. a<y ∧ y<x}"
      define c where "c≡ (if cs = {} then (x+a)/2 else Max cs)"
      have "finite cs" unfolding cs_def using assms(1) by auto
      have "c<x ∧ (∀y. c<y ∧ y<x ⟶ f y=g y)" 
      proof (cases "cs={}")
        case True
        then have "∀y. c<y ∧ y<x ⟶ y ∉ s" unfolding cs_def c_def by force
        moreover have "c=(x+a)/2" using True unfolding c_def by auto
        ultimately show ?thesis using fg_eq using that by auto
      next
        case False
        then have "c∈cs" unfolding c_def using False ‹finite cs› by auto
        moreover have "∀y. c<y ∧ y<x ⟶ y ∉ s" 
        proof (rule ccontr)
          assume "¬ (∀y. c < y ∧ y < x ⟶ y ∉ s) "
          then obtain y' where "c<y'" "y'<x" "y'∈s" by auto
          then have "y'∈cs" using ‹c∈cs› unfolding cs_def by auto
          then have "y'≤c" unfolding c_def using False ‹finite cs› by auto
          then show False using ‹c<y'› by auto
        qed
        ultimately show ?thesis unfolding cs_def using that by (auto intro!:fg_eq)
      qed  
      then show "∀F x in at_left x. f x = g x"
        unfolding eventually_at_left by auto
    qed simp
    then show ?thesis
      unfolding left_def
      by (auto intro: sum.cong)
  qed
  moreover have "right f = right g"
  proof -
    have "jumpF f (at_right x) = jumpF g (at_right x)" when "a≤x" "x<b" for x 
    proof (rule jumpF_cong)
      define cs where "cs ≡ {y∈s. x<y ∧ y<b}"
      define c where "c≡ (if cs = {} then (x+b)/2 else Min cs)"
      have "finite cs" unfolding cs_def using assms(1) by auto
      have "x<c ∧ (∀y. x<y ∧ y<c ⟶ f y=g y)" 
      proof (cases "cs={}")
        case True
        then have "∀y. x<y ∧ y<c ⟶ y ∉ s" unfolding cs_def c_def by force
        moreover have "c=(x+b)/2" using True unfolding c_def by auto
        ultimately show ?thesis using fg_eq using that by auto
      next
        case False
        then have "c∈cs" unfolding c_def using False ‹finite cs› by auto
        moreover have "∀y. x<y ∧ y<c ⟶ y ∉ s" 
        proof (rule ccontr)
          assume "¬ (∀y. x < y ∧ y < c ⟶ y ∉ s) "
          then obtain y' where "x<y'" "y'<c" "y'∈s" by auto
          then have "y'∈cs" using ‹c∈cs› unfolding cs_def by auto
          then have "y'≥c" unfolding c_def using False ‹finite cs› by auto
          then show False using ‹c>y'› by auto
        qed
        ultimately show ?thesis unfolding cs_def using that by (auto intro!:fg_eq)
      qed  
      then show "∀F x in at_right x. f x = g x"
        unfolding eventually_at_right by auto
    qed simp
    then show ?thesis
      unfolding right_def
      by (auto intro: sum.cong)
  qed
  ultimately show ?thesis unfolding cindexE_def left_def right_def by presburger
qed
      
lemma cindexE_constI:
  assumes "⋀t. ⟦a<t;t<b⟧ ⟹ f t=c"
  shows "cindexE a b f = 0"
proof -
  define left where 
      "left=(λf. (∑x | jumpF f (at_left x) ≠ 0 ∧ a < x ∧ x ≤ b. jumpF f (at_left x)))"
  define right where 
      "right=(λf. (∑x | jumpF f (at_right x) ≠ 0 ∧ a ≤ x ∧ x < b. jumpF f (at_right x)))"
  have "left f = 0"  
  proof -
    have "jumpF f (at_left x) = 0" when "a<x" "x≤b" for x 
      apply (rule jumpF_eventually_const[of _ c])
      unfolding eventually_at_left using assms that by auto
    then show ?thesis unfolding left_def by auto
  qed
  moreover have "right f = 0"  
  proof -
    have "jumpF f (at_right x) = 0" when "a≤x" "x<b" for x 
      apply (rule jumpF_eventually_const[of _ c])
      unfolding eventually_at_right using assms that by auto
    then show ?thesis unfolding right_def by auto
  qed
  ultimately show ?thesis unfolding cindexE_def left_def right_def by auto
qed

lemma cindex_eq_cindexE_divide:
  fixes f g::"real ⇒ real"
  defines "h ≡ (λx. f x/g x)"
  assumes "a<b" and
    finite_fg: "finite {x. (f x=0∨g x=0) ∧ a≤x∧x≤b}" and 
    g_imp_f:"∀x∈{a..b}. g x=0 ⟶ f x≠0" and
    f_cont:"continuous_on {a..b} f" and
    g_cont:"continuous_on {a..b} g"
  shows "cindexE a b h = jumpF h (at_right a) + cindex a