Theory Poincare_Bendixson.Poincare_Bendixson

section ‹Poincare Bendixson Theory›
theory Poincare_Bendixson
  imports 
    Ordinary_Differential_Equations.ODE_Analysis
    Analysis_Misc ODE_Misc Periodic_Orbit
begin


subsection ‹Flow to Path›

context auto_ll_on_open begin

(* The path along the flow starting at time t to time t' *)
definition "flow_to_path x t t' = flow0 x  linepath t t'"

lemma pathstart_flow_to_path[simp]:
  shows "pathstart (flow_to_path x t t') = flow0 x t"
  unfolding flow_to_path_def
  by (auto simp add: pathstart_compose)

lemma pathfinish_flow_to_path[simp]:
  shows "pathfinish (flow_to_path x t t') = flow0 x t'"
  unfolding flow_to_path_def
  by (auto simp add: pathfinish_compose)

lemma flow_to_path_unfold:
  shows "flow_to_path x t t' s = flow0 x ((1 - s) * t + s * t')"
  unfolding flow_to_path_def o_def linepath_def by auto

lemma subpath0_flow_to_path:
  shows "(subpath 0 u (flow_to_path x t t')) = flow_to_path x t (t + u*(t'-t))"
  unfolding flow_to_path_def subpath_image subpath0_linepath
  by auto

lemma path_image_flow_to_path[simp]:
  assumes "t  t'"
  shows "path_image (flow_to_path x t t') = flow0 x ` {t..t'}"
  unfolding flow_to_path_def path_image_compose path_image_linepath
  using assms real_Icc_closed_segment by auto

lemma flow_to_path_image0_right_open[simp]:
  assumes "t < t'"
  shows "flow_to_path x t t' ` {0..<1} = flow0 x `{t..<t'}"
  unfolding flow_to_path_def image_comp[symmetric] linepath_image0_right_open_real[OF assms]
  by auto

lemma flow_to_path_path:
  assumes "t  t'"
  assumes "{t..t'}  existence_ivl0 x"
  shows "path (flow_to_path x t t')"
proof -
  have "x  X"
    using assms(1) assms(2) subset_empty by fastforce
  have "xa. 0  xa  xa  1   (1 - xa) * t + xa * t'  t'"
    by (simp add: assms(1) convex_bound_le)
  moreover have "xa. 0  xa  xa  1  t  (1 - xa) * t + xa * t'" using assms(1)
    by (metis add.commute add_diff_cancel_left' diff_diff_eq2 diff_le_eq mult.commute mult.right_neutral mult_right_mono right_diff_distrib')
  ultimately have "xa. 0  xa  xa  1  (1 - xa) * t + xa * t'  existence_ivl0 x"
    using assms(2) by auto
  thus ?thesis unfolding path_def flow_to_path_def linepath_def
    by (auto intro!:continuous_intros simp add :x  X)
qed

lemma flow_to_path_arc:
  assumes "t  t'"
  assumes "{t..t'}  existence_ivl0 x"
  assumes "s  {t<..<t'}. flow0 x s  flow0 x t"
  assumes "flow0 x t  flow0 x t'"
  shows "arc (flow_to_path x t t')"
  unfolding arc_def
proof safe
  from flow_to_path_path[OF assms(1-2)]
  show "path (flow_to_path x t t')" .
next
  show "inj_on (flow_to_path x t t') {0..1}"
    unfolding flow_to_path_def
    apply (rule comp_inj_on)
     apply (metis assms(4) inj_on_linepath)
    using assms path_image_linepath[of t t'] apply (auto intro!:flow0_inj_on)
    using flow0_inj_on greaterThanLessThan_iff linepath_image_01 real_Icc_closed_segment by fastforce
qed

end

locale c1_on_open_R2 = c1_on_open_euclidean f f' X for f::"'a::executable_euclidean_space  _" and f' and X +
  assumes dim2: "DIM('a) = 2"
begin


subsection ‹2D Line segments›

text ‹Line segments are specified by two endpoints
      The closed line segment from x to y is given by the set {x--y}
      and {x<--<y} for the open segment›

text ‹ Rotates a vector clockwise 90 degrees ›
definition "rot (v::'a) = (eucl_of_list [nth_eucl v 1, -nth_eucl v 0]::'a)"

lemma exhaust2_nat: "(i<(2::nat). P i)  P 0  P 1"
  using less_2_cases by auto
lemma sum2_nat: "(i<(2::nat). P i) = P 0 + P 1"
  by (simp add: eval_nat_numeral)

lemmas vec_simps =
  eucl_eq_iff[where 'a='a] dim2 eucl_of_list_eucl_nth exhaust2_nat
  plus_nth_eucl
  minus_nth_eucl
  uminus_nth_eucl
  scaleR_nth_eucl
  inner_nth_eucl
  sum2_nat
  algebra_simps

lemma minus_expand:
  shows "(x::'a)-y = (eucl_of_list [x$e0 - y$e0, x$e1 - y$e1])"
  by (simp add:vec_simps)

lemma dot_ortho[simp]: "x  rot x = 0"
  unfolding rot_def minus_expand
  by (simp add: vec_simps)

lemma nrm_dot:
  shows "((x::'a)-y)  (rot (x-y)) = 0"
  unfolding rot_def minus_expand
  by (simp add: vec_simps)

lemma nrm_reverse: "a  (rot (x-y)) = - a  (rot (y-x))" for x y::'a
  unfolding rot_def
  by (simp add:vec_simps)

lemma norm_rot: "norm (rot v) = norm v" for v::'a
  unfolding rot_def
  by (simp add:vec_simps norm_nth_eucl L2_set_def)

lemma rot_rot[simp]:
  shows "rot (rot v) = -v"
  unfolding rot_def
  by (simp add:vec_simps)

lemma rot_scaleR[simp]:
  shows "rot ( u *R v) =  u *R (rot v)"
  unfolding rot_def
  by (simp add:vec_simps)

lemma rot_0[simp]: "rot 0 = 0"
  using rot_scaleR[of 0] by simp

lemma rot_eq_0_iff[simp]: "rot x = 0  x = 0"
  apply (auto simp: rot_def)
   apply (metis One_nat_def norm_eq_zero norm_rot norm_zero rot_def)
  using rot_0 rot_def by auto

lemma in_segment_inner_rot:
  "(x - a)  rot (b - a) = 0"
  if "x  {a--b}"
proof -
  from that obtain u where x: "x = a + u *R (b - a)" "0  u" "u  1"
    by (auto simp: in_segment algebra_simps)
  show ?thesis
    unfolding x
    by (simp add: inner_add_left nrm_dot)
qed

lemma inner_rot_in_segment:
  "x  range (λu. a + u *R (b - a))"
  if "(x - a)  rot (b - a) = 0" "a  b"
proof -
  from that have
    x0: "b $e 0 = a $e 0  x $e 0 =
      (a $e 0 * b $e Suc 0 - b $e 0 * a $e Suc 0 + (b $e 0 - a $e 0) * x $e Suc 0) /
      (b $e Suc 0 - a $e Suc 0)"
    and x1: "b $e 0  a $e 0  x $e Suc 0 =
      ((b $e Suc 0 - a $e Suc 0) * x $e 0 - a $e 0 * b $e Suc 0 + b $e 0 * a $e Suc 0) / (b $e 0 - a $e 0)"
    by (auto simp: rot_def vec_simps divide_simps)
  define u where "u = (if b $e 0 - a $e 0  0
    then ((x $e 0 - a $e 0) / (b $e 0 -  a $e 0))
    else ((x $e 1 - a $e 1) / (b $e 1 -  a $e 1)))
    "
  show ?thesis
    apply (cases "b $e 0 - a $e 0 = 0")
    subgoal
      using that(2)
      apply (auto intro!: image_eqI[where x="((x $e 1 - a $e 1) / (b $e 1 -  a $e 1))"]
          simp: vec_simps x0 divide_simps algebra_simps)
       apply (metis ab_semigroup_mult_class.mult_ac(1) mult.commute sum_sqs_eq)
      by (metis mult.commute mult.left_commute sum_sqs_eq)
    subgoal
      apply (auto intro!: image_eqI[where x="((x $e 0 - a $e 0) / (b $e 0 -  a $e 0))"]
          simp: vec_simps x1 divide_simps algebra_simps)
       apply (metis ab_semigroup_mult_class.mult_ac(1) mult.commute sum_sqs_eq)
      by (metis mult.commute mult.left_commute sum_sqs_eq)
    done
qed

lemma in_open_segment_iff_rot:
  "x  {a<--<b}  (x - a)  rot (b - a) = 0  x  (b - a)  {a(b - a) <..< b  (b - a)}"
  if "a  b"
  unfolding open_segment_line_hyperplanes[OF that]
  by (auto simp: nrm_dot intro!: inner_rot_in_segment)

lemma in_open_segment_rotD:
  "x  {a<--<b}  (x - a)  rot (b - a) = 0  x  (b - a)  {a(b - a) <..< b  (b - a)}"
  by (subst in_open_segment_iff_rot[symmetric]) auto

lemma in_closed_segment_iff_rot:
  "x  {a--b}  (x - a)  rot (b - a) = 0  x  (b - a)  {a(b - a) .. b  (b - a)}"
  if "a  b"
  unfolding closed_segment_line_hyperplanes[OF that] using that
  by (auto simp: nrm_dot intro!: inner_rot_in_segment)

lemma in_segment_inner_rot2:
  "(x - y)  rot (a - b) = 0"
  if "x  {a--b}" "y  {a--b}"
proof -
  from that obtain u where x: "x = a + u *R (b - a)" "0  u" "u  1"
    by (auto simp: in_segment algebra_simps)
  from that obtain v where y: "y = a + v *R (b - a)" "0  v" "v  1"
    by (auto simp: in_segment algebra_simps)
  show ?thesis
    unfolding x y
    apply (auto simp: inner_add_left )
    by (smt add_diff_cancel_left' in_segment_inner_rot inner_diff_left minus_diff_eq nrm_reverse that(1) that(2) x(1) y(1))
qed

lemma closed_segment_surface:
  "a  b  {a--b} = { x  {x. x  (b - a)  {a(b - a) .. b  (b - a)}}. (x - a)  rot (b - a) = 0}"
  by (auto simp: in_closed_segment_iff_rot)

lemma rot_diff_commute: "rot (b - a) = -rot(a - b)"
  apply (auto simp: rot_def algebra_simps)
  by (metis One_nat_def minus_diff_eq rot_def rot_rot)


subsection ‹Bijection Real-Complex for Jordan Curve Theorem›

definition "complex_of (x::'a) = x$e0 + 𝗂 * x$e1"

definition "real_of (x::complex) = (eucl_of_list [Re x, Im x]::'a)"

lemma complex_of_linear:
  shows "linear complex_of"
  unfolding complex_of_def
  apply (auto intro!:linearI simp add: distrib_left plus_nth_eucl)
  by (simp add: of_real_def scaleR_add_right scaleR_nth_eucl)

lemma complex_of_bounded_linear:
  shows "bounded_linear complex_of"
  unfolding complex_of_def
  apply (auto intro!:bounded_linearI' simp add: distrib_left plus_nth_eucl)
  by (simp add: of_real_def scaleR_add_right scaleR_nth_eucl)

lemma real_of_linear:
  shows "linear real_of"
  unfolding real_of_def
  by (auto intro!:linearI simp add: vec_simps)

lemma real_of_bounded_linear:
  shows "bounded_linear real_of"
  unfolding real_of_def
  by (auto intro!:bounded_linearI' simp add: vec_simps)

lemma complex_of_real_of:
  "(complex_of  real_of) = id"
  unfolding complex_of_def real_of_def
  using complex_eq by (auto simp add:vec_simps)

lemma real_of_complex_of:
  "(real_of  complex_of) = id"
  unfolding complex_of_def real_of_def
  using complex_eq by (auto simp add:vec_simps)

lemma complex_of_bij:
  shows "bij (complex_of)"
  using o_bij[OF real_of_complex_of complex_of_real_of] .

lemma real_of_bij:
  shows "bij (real_of)"
  using o_bij[OF complex_of_real_of real_of_complex_of] .

lemma real_of_inj:
  shows "inj (real_of)"
  using real_of_bij
  using bij_betw_imp_inj_on by auto

lemma Jordan_curve_R2:
  fixes c :: "real  'a"
  assumes "simple_path c" "pathfinish c = pathstart c"
  obtains inside outside where
    "inside  {}" "open inside" "connected inside"
    "outside  {}" "open outside" "connected outside"
    "bounded inside" "¬ bounded outside"
    "inside  outside = {}"
    "inside  outside = - path_image c"
    "frontier inside = path_image c"
    "frontier outside = path_image c"
proof -
  from simple_path_linear_image_eq[OF complex_of_linear]
  have a1:"simple_path (complex_of  c)" using assms(1) complex_of_bij
    using bij_betw_imp_inj_on by blast
  have a2:"pathfinish (complex_of  c) = pathstart (complex_of  c)"
    using assms(2) by (simp add:pathstart_compose pathfinish_compose)

  from Jordan_curve[OF a1 a2]
  obtain inside outside where io:
    "inside  {}" "open inside" "connected inside"
    "outside  {}" "open outside" "connected outside"
    "bounded inside" "¬ bounded outside" "inside  outside = {}"
    "inside  outside = - path_image (complex_of  c)"
    "frontier inside = path_image (complex_of  c)"
    "frontier outside = path_image (complex_of  c)" by blast
  let ?rin = "real_of ` inside"
  let ?rout = "real_of ` outside"
  have i: "inside = complex_of ` ?rin" using complex_of_real_of unfolding image_comp
    by auto
  have o: "outside = complex_of ` ?rout" using complex_of_real_of unfolding image_comp
    by auto
  have c: "path_image(complex_of  c) = complex_of ` (path_image c)"
    by (simp add: path_image_compose)
  have "?rin  {}" using io by auto
  moreover from open_bijective_linear_image_eq[OF real_of_linear real_of_bij]
  have "open ?rin" using io by auto
  moreover from connected_linear_image[OF real_of_linear]
  have "connected ?rin" using io by auto
  moreover have "?rout  {}" using io by auto
  moreover from open_bijective_linear_image_eq[OF real_of_linear real_of_bij]
  have "open ?rout" using io by auto
  moreover from connected_linear_image[OF real_of_linear]
  have "connected ?rout" using io by auto
  moreover from bounded_linear_image[OF io(7) real_of_bounded_linear]
  have "bounded ?rin" .
  moreover from bounded_linear_image[OF _ complex_of_bounded_linear]
  have "¬ bounded ?rout" using io(8) o
    by force
  from image_Int[OF real_of_inj]
  have "?rin  ?rout = {}" using io(9) by auto
  moreover from bij_image_Compl_eq[OF complex_of_bij]
  have "?rin  ?rout = - path_image c" using io(10) unfolding c
    by (metis id_apply image_Un image_comp image_cong image_ident real_of_complex_of)
  moreover from closure_injective_linear_image[OF real_of_linear real_of_inj]
  have "frontier ?rin = path_image c" using io(11)
    unfolding frontier_closures c
    by (metis B A. real_of ` (A  B) = real_of ` A  real_of ` B bij_image_Compl_eq c calculation(9) compl_sup double_compl io(10) real_of_bij)
  moreover from closure_injective_linear_image[OF real_of_linear real_of_inj]
  have "frontier ?rout = path_image c" using io(12)
    unfolding frontier_closures c
    by (metis B A. real_of ` (A  B) = real_of ` A  real_of ` B bij_image_Compl_eq c calculation(10) frontier_closures io(11) real_of_bij)
  ultimately show ?thesis
    by (meson ¬ bounded (real_of ` outside) that)
qed

(* copied *)
corollary Jordan_inside_outside_R2:
  fixes c :: "real  'a"
  assumes "simple_path c" "pathfinish c = pathstart c"
  shows "inside(path_image c)  {} 
          open(inside(path_image c)) 
          connected(inside(path_image c)) 
          outside(path_image c)  {} 
          open(outside(path_image c)) 
          connected(outside(path_image c)) 
          bounded(inside(path_image c)) 
          ¬ bounded(outside(path_image c)) 
          inside(path_image c)  outside(path_image c) = {} 
          inside(path_image c)  outside(path_image c) =
          - path_image c 
          frontier(inside(path_image c)) = path_image c 
          frontier(outside(path_image c)) = path_image c"
proof -
  obtain inner outer
    where *: "inner  {}" "open inner" "connected inner"
      "outer  {}" "open outer" "connected outer"
      "bounded inner" "¬ bounded outer" "inner  outer = {}"
      "inner  outer = - path_image c"
      "frontier inner = path_image c"
      "frontier outer = path_image c"
    using Jordan_curve_R2 [OF assms] by blast
  then have inner: "inside(path_image c) = inner"
    by (metis dual_order.antisym inside_subset interior_eq interior_inside_frontier)
  have outer: "outside(path_image c) = outer"
    using inner  outer = - path_image c inside (path_image c) = inner
      outside_inside inner  outer = {} by auto
  show ?thesis
    using * by (auto simp: inner outer)
qed

lemma jordan_points_inside_outside:
  fixes p :: "real  'a"
  assumes "0 < e"
  assumes jordan: "simple_path p" "pathfinish p = pathstart p"
  assumes x: "x  path_image p"
  obtains y z where "y  inside (path_image p)" "y  ball x e" 
    "z  outside (path_image p)" "z  ball x e"
proof -
  from Jordan_inside_outside_R2[OF jordan]
  have xi: "x  frontier(inside (path_image p))" and
    xo: "x  frontier(outside (path_image p))"
    using x by auto
  obtain y where y:"y  inside (path_image p)" "y  ball x e" using 0 < e xi
    unfolding frontier_straddle
    by auto
  obtain z where z:"z  outside (path_image p)" "z  ball x e" using 0 < e xo
    unfolding frontier_straddle
    by auto
  show ?thesis using y z that by blast
qed  

lemma eventually_at_open_segment:
  assumes "x  {a<--<b}"
  shows "F y in at x. (y-a)  rot(a-b) = 0  y  {a <--< b}"
proof -
  from assms have "a  b" by auto
  from assms have x: "(x - a)  rot (b - a) = 0" "x  (b - a)  {a  (b - a)<..<b  (b - a)}"
    unfolding in_open_segment_iff_rot[OF a  b]
    by auto
  then have "F y in at x. y  (b - a)  {a  (b - a)<..<b  (b - a)}"
    by (intro topological_tendstoD) (auto intro!: tendsto_intros)
  then show ?thesis
    by eventually_elim (auto simp: in_open_segment_iff_rot[OF a  b] nrm_reverse[of _ a b] algebra_simps dist_commute)
qed

lemma linepath_ball:
  assumes "x  {a<--<b}"
  obtains e where "e > 0" "ball x e  {y. (y-a)  rot(a-b) = 0}  {a <--< b}"
proof -
  from eventually_at_open_segment[OF assms] assms
  obtain e where "0 < e" "ball x e  {y. (y - a)  rot (a - b) = 0}  {a<--<b}"
    by (force simp: eventually_at in_open_segment_iff_rot dist_commute)
  then show ?thesis ..
qed

lemma linepath_ball_inside_outside:
  fixes p :: "real  'a"
  assumes jordan: "simple_path (p +++ linepath a b)" "pathfinish p = a" "pathstart p = b"
  assumes x: "x  {a<--<b}"
  obtains e where "e > 0" "ball x e  path_image p = {}"
    "ball x e  {y. (y-a)  rot (a-b) > 0}  inside (path_image (p +++ linepath a b)) 
     ball x e  {y. (y-a)  rot (a-b) < 0}  outside (path_image (p +++ linepath a b))
      
     ball x e  {y. (y-a)  rot (a-b) < 0}  inside (path_image (p +++ linepath a b)) 
     ball x e  {y. (y-a)  rot (a-b) > 0}  outside (path_image (p +++ linepath a b))"
proof -
  let ?lp = "p +++ linepath a b"
  have "a  b" using x by auto
  have pp:"path p" using jordan path_join pathfinish_linepath simple_path_imp_path
    by fastforce
  have "path_image p  path_image (linepath a b)  {a,b}"
    using jordan simple_path_join_loop_eq
    by (metis (no_types, lifting) inf_sup_aci(1) insert_commute path_join_path_ends path_linepath simple_path_imp_path simple_path_joinE)
  then have "x  path_image p" using x unfolding path_image_linepath
    by (metis DiffE Int_iff le_iff_inf open_segment_def)
  then have "F y in at x. y  path_image p"
    by (intro eventually_not_in_closed) (auto simp: closed_path_image path p)
  moreover 
  have "F y in at x. (y - a)  rot (a - b) = 0  y  {a<--<b}"
    by (rule eventually_at_open_segment[OF x])
  ultimately have "F y in at x. y  path_image p  ((y - a)  rot (a - b) = 0  y  {a<--<b})"
    by eventually_elim auto
  then obtain e where e: "e > 0" "ball x e  path_image p = {}"
    "ball x e  {y. (y - a)  rot (a - b) = 0}  {a<--<b}"
    using x  path_image p x in_open_segment_rotD[OF x]
    apply (auto simp: eventually_at subset_iff dist_commute dest!: )
    by (metis Int_iff all_not_in_conv dist_commute mem_ball) 
  have a1: "pathfinish ?lp = pathstart ?lp"
    by (auto simp add: jordan)
  have "x  path_image ?lp"
    using jordan(1) open_closed_segment path_image_join path_join_path_ends simple_path_imp_path x by fastforce
  from jordan_points_inside_outside[OF e(1) jordan(1) a1 this]
  obtain y z where y: "y  inside (path_image ?lp)" "y  ball x e" 
    and z: "z  outside (path_image ?lp)" "z  ball x e" by blast
  have jordancurve:
    "inside (path_image ?lp)  outside(path_image ?lp) = {}"
    "frontier (inside (path_image ?lp)) = path_image ?lp"
    "frontier (outside (path_image ?lp)) = path_image ?lp"
    using Jordan_inside_outside_R2[OF jordan(1) a1] by auto
  define b1 where "b1 = ball x e  {y. (y-a)  rot (a-b) > 0}"
  define b2 where "b2 = ball x e  {y. (y-a)  rot (a-b) < 0}"
  define b3 where "b3 = ball x e  {y. (y-a)  rot (a-b) = 0}"
  have "path_connected b1" unfolding b1_def
    apply (auto intro!: convex_imp_path_connected convex_Int simp add:inner_diff_left)
    using convex_halfspace_gt[of "a  rot (a - b)" "rot(a-b)"] inner_commute
    by (metis (no_types, lifting) Collect_cong)
  have "path_connected b2" unfolding b2_def
    apply (auto intro!: convex_imp_path_connected convex_Int simp add:inner_diff_left)
    using convex_halfspace_lt[of "rot(a-b)" "a  rot (a - b)"] inner_commute
    by (metis (no_types, lifting) Collect_cong)
  have "b1  path_image(linepath a b) = {}" unfolding path_image_linepath b1_def
    using closed_segment_surface[OF a  b] in_segment_inner_rot2 by auto 
  then have b1i:"b1  path_image ?lp = {}"
    by (metis IntD2 b1_def disjoint_iff_not_equal e(2) inf_sup_aci(1) not_in_path_image_join)
  have "b2  path_image(linepath a b) = {}" unfolding path_image_linepath b2_def
    using closed_segment_surface[OF a  b] in_segment_inner_rot2 by auto 
  then have b2i:"b2  path_image ?lp = {}"
    by (metis IntD2 b2_def disjoint_iff_not_equal e(2) inf_sup_aci(1) not_in_path_image_join)
  have bsplit: "ball x e = b1  b2  b3"
    unfolding b1_def b2_def b3_def
    by auto
  have "z  b3"
  proof clarsimp
    assume "z  b3"
    then have "z  {a<--<b}" unfolding b3_def using e by blast
    then have "z  path_image(linepath a b)" by (auto simp add: open_segment_def)
    then have "z  path_image ?lp"
      by (simp add: jordan(2) path_image_join)
    thus False using z
      using inside_Un_outside by fastforce
  qed
  then have z12: "z  b1  z  b2" using z bsplit by blast
  have "y  b3"
  proof clarsimp
    assume "y  b3"
    then have "y  {a<--<b}" unfolding b3_def using e by auto
    then have "y  path_image(linepath a b)" by (auto simp add: open_segment_def)
    then have "y  path_image ?lp"
      by (simp add: jordan(2) path_image_join)
    thus False using y
      using inside_Un_outside by fastforce
  qed
  then have "y  b1  y  b2" using y bsplit by blast
  moreover {
    assume "y  b1"
    then have "b1  inside (path_image ?lp)  {}" using y by blast
    from path_connected_not_frontier_subset[OF path_connected b1 this]
    have 1:"b1  inside (path_image ?lp)" unfolding jordancurve using b1i
      by blast
    then have "z  b2" using jordancurve(1) z(1) z12 by blast
    then have "b2  outside (path_image ?lp)  {}" using z by blast
    from path_connected_not_frontier_subset[OF path_connected b2 this]
    have 2:"b2  outside (path_image ?lp)" unfolding jordancurve using b2i
      by blast
    note conjI[OF 1 2]
  }
  moreover {
    assume "y  b2"
    then have "b2  inside (path_image ?lp)  {}" using y by blast
    from path_connected_not_frontier_subset[OF path_connected b2 this]
    have 1:"b2  inside (path_image ?lp)" unfolding jordancurve using b2i
      by blast
    then have "z  b1" using jordancurve(1) z(1) z12 by blast
    then have "b1  outside (path_image ?lp)  {}" using z by blast
    from path_connected_not_frontier_subset[OF path_connected b1 this]
    have 2:"b1  outside (path_image ?lp)" unfolding jordancurve using b1i
      by blast
    note conjI[OF 1 2]
  } 
  ultimately show ?thesis unfolding b1_def b2_def using that[OF e(1-2)] by auto
qed

subsection ‹Transversal Segments›― ‹TODO: Transversal surface in Euclidean space?!›

definition "transversal_segment a b 
  a  b  {a--b}  X 
  (z  {a--b}. f z  rot (a-b)  0)"

lemma transversal_segment_reverse:
  assumes "transversal_segment x y"
  shows "transversal_segment y x"
  unfolding transversal_segment_def
  by (metis (no_types, opaque_lifting) add.left_neutral add_uminus_conv_diff assms closed_segment_commute inner_diff_left inner_zero_left nrm_reverse transversal_segment_def) 

lemma transversal_segment_commute: "transversal_segment x y  transversal_segment y x"
  using transversal_segment_reverse by blast

lemma transversal_segment_neg:
  assumes "transversal_segment x y"
  assumes w: "w  {x -- y}" and "f w  rot (x-y) < 0"
  shows "z  {x--y}. f(z)  rot (x-y) < 0"
proof (rule ccontr)
  assume " ¬ (z{x--y}. f z  rot (x-y) < 0)"
  then obtain z where z: "z  {x--y}" "f z  rot (x-y)  0" by auto
  define ff where "ff = (λs. f (w + s *R (z - w))  rot (x-y))"
  have f0:"ff 0  0" unfolding ff_def using assms(3)
    by simp 
  have fu:"ff 1  0"
    by (auto simp: ff_def z)
  from assms(2) obtain u where u: "0  u" "u  1" "w = (1 - u) *R x + u *R y"
    unfolding in_segment by blast
  have "{x--y}  X" using assms(1) unfolding transversal_segment_def by blast
  then have "continuous_on {0..1} ff" unfolding ff_def 
    using assms(2)
    by (auto intro!:continuous_intros closed_subsegmentI z elim!: set_mp)
  from IVT'[of ff, OF f0 fu zero_le_one this]
  obtain s where s: "s  0" "s  1" "ff s = 0" by blast
  have "w + s *R (z - w)  {x -- y}"
    by (auto intro!: closed_subsegmentI z s w)
  with ff s = 0 show False
    using s assms(1) unfolding transversal_segment_def ff_def by blast
qed

lemmas transversal_segment_sign_less = transversal_segment_neg[OF _ ends_in_segment(1)]

lemma transversal_segment_pos:
  assumes "transversal_segment x y"
  assumes w: "w  {x -- y}" "f w  rot (x-y) > 0"
  shows "z  {x--y}. f(z)  rot (x-y) > 0"
  using transversal_segment_neg[OF transversal_segment_reverse[OF assms(1)], of w] w
  by (auto simp: rot_diff_commute[of x y] closed_segment_commute)

lemma transversal_segment_posD:
  assumes "transversal_segment x y"
    and pos: "z  {x -- y}" "f z  rot (x - y) > 0"
  shows "x  y" "{x--y}  X" "z. z  {x--y}  f z  rot (x-y) > 0"
  using assms(1) transversal_segment_pos[OF assms]
  by (auto simp: transversal_segment_def)

lemma transversal_segment_negD:
  assumes "transversal_segment x y"
    and pos: "z  {x -- y}" "f z  rot (x - y) < 0"
  shows "x  y" "{x--y}  X" "z. z  {x--y}  f z  rot (x-y) < 0"
  using assms(1) transversal_segment_neg[OF assms]
  by (auto simp: transversal_segment_def)

lemma transversal_segmentE:
  assumes "transversal_segment x y"
  obtains "x  y" "{x -- y}  X" "z. z  {x--y}  f z  rot (x - y) > 0"
  |  "x  y" "{x -- y}  X" "z. z  {x--y}  f z  rot (y - x) > 0"
proof (cases "f x  rot (x - y) < 0")
  case True
  from transversal_segment_negD[OF assms ends_in_segment(1) True]
  have "x  y" "{x -- y}  X" "z. z  {x--y}  f z  rot (y - x) > 0"
    by (auto simp: rot_diff_commute[of x y])
  then show ?thesis ..
next
  case False
  then have "f x  rot (x - y) > 0" using assms
    by (auto simp: transversal_segment_def algebra_split_simps not_less order.order_iff_strict)
  from transversal_segment_posD[OF assms ends_in_segment(1) this]
  show ?thesis ..
qed

lemma dist_add_vec:
  shows "dist (x + s *R v) x = abs s * norm v"
  by (simp add: dist_cancel_add1)

lemma transversal_segment_exists:
  assumes "x  X" "f x  0"
  obtains a b where "x  {a<--<b}"
    "transversal_segment a b"
proof -
  (* Line through x perpendicular to f x *)
  define l where "l = (λs::real. x + (s/norm(f x)) *R rot (f x))"
  have "norm (f x) > 0" using assms(2) using zero_less_norm_iff by blast 
  then have distl: "s. dist (l s) x = abs s" unfolding l_def dist_add_vec
    by (auto simp add: norm_rot)
  obtain d where d:"d > 0" "cball x d  X"
    by (meson UNIV_I assms(1) local.local_unique_solution)
  then have lb: "l`{-d..d}  cball x d" using distl by (simp add: abs_le_iff dist_commute image_subset_iff)
  from fcontx[OF assms(1)] have "continuous (at x) f" .
  then have c:"continuous (at 0) ((λy. (f y  f x))  l)" unfolding l_def
    by (auto intro!:continuous_intros simp add: assms(2))
  have "((λy. f y  f x)  l) 0 > 0" using assms(2) unfolding l_def o_def by auto
  from continuous_at_imp_cball[OF c this]
  obtain r where r:"r > 0" " zcball 0 r. 0 < ((λy. f y  f x)  l) z" by blast
  then have rc:"z  l`{-r..r}. 0 < f z  f x" using real_norm_def by auto 
  define dr where "dr = min r d"
  have t1:"l (-dr)  l dr" unfolding l_def dr_def
    by (smt 0 < d 0 < norm (f x) 0 < r add_left_imp_eq divide_cancel_right norm_rot norm_zero scale_cancel_right)
  have "x = midpoint (l (-dr)) (l dr)" unfolding midpoint_def l_def by auto
  then have xin:"x  {l (-dr)<--<(l dr)}" using t1 by auto
      (* TODO: actually this should be equality, but l is affine ...
     also the existing stuff about -- is a little too specific *)
  have lsub:"{l (-dr)--l dr}  l`{-dr..dr}"
  proof safe
    fix z
    assume "z  {l (- dr)--l dr}"
    then obtain u where u: "0  u" "u  1" "z = (1 - u) *R (l (-dr)) + u *R (l dr)"
      unfolding in_segment by blast
    then have "z = x - (1-u) *R (dr/norm(f x)) *R rot (f x) + u *R  (dr/norm(f x)) *R rot (f x) "
      unfolding l_def
      by (simp add: l_def scaleR_add_right scale_right_diff_distrib u(3))
    also have "... = x - (1 - 2 * u) *R (dr/norm(f x)) *R rot (f x)"
      by (auto simp add: algebra_simps divide_simps simp flip: scaleR_add_left)
    also have "... =  x + (((2 * u - 1) * dr)/norm(f x)) *R rot (f x)"
      by (smt add_uminus_conv_diff scaleR_scaleR scale_minus_left times_divide_eq_right)
    finally have zeq: "z = l ((2*u-1)*dr)" unfolding l_def .
    have ub: " 2* u - 1  1  -1   2* u - 1 " using u by linarith
    thus "z  l ` {- dr..dr}" using zeq
      by (smt atLeastAtMost_iff d(1) dr_def image_eqI mult.commute mult_left_le mult_minus_left r(1)) 
  qed
  have t2: "{l (- dr)--l dr}  X" using lsub
    by (smt atLeastAtMost_iff d(2) dist_commute distl dr_def image_subset_iff mem_cball order_trans)
  have "l (- dr) - l dr = -2 *R (dr/norm(f x)) *R rot (f x)" unfolding l_def
    by (simp add: algebra_simps flip: scaleR_add_left)
  then have req: "rot (l (- dr) - l dr) = (2 * dr/norm(f x)) *R f x"
    by auto (metis add.inverse_inverse rot_rot rot_scaleR)
  have "l`{-dr..dr}  l ` {-r ..r}"
    by (simp add: dr_def image_mono)
  then have "{l (- dr)--l dr}  l ` {-r .. r}" using lsub by auto
  then have "z  {l (- dr)--l dr}. 0 < f z  f x" using rc by blast
  moreover have "(dr / norm (f x)) > 0"
    using 0 < norm (f x) d(1) dr_def r(1) by auto 
  ultimately have t3: "z  {l (- dr)--l dr}. f z  rot (l (- dr)- l dr) > 0" unfolding req
    by (smt divide_divide_eq_right inner_scaleR_right mult_2 norm_not_less_zero scaleR_2 times_divide_eq_left times_divide_eq_right zero_less_divide_iff)
  have "transversal_segment (l (-dr)) (l dr)" using t1 t2 t3 unfolding transversal_segment_def by auto
  thus ?thesis using xin
    using that by auto 
qed

text ‹Perko Section 3.7 Lemma 2 part 1.› 
lemma flow_transversal_segment_finite_intersections:
  assumes "transversal_segment a b"
  assumes "t  t'" "{t .. t'}  existence_ivl0 x"
  shows "finite {s{t..t'}. flow0 x s  {a--b}}"
proof -
  from assms have "a  b" by (simp add: transversal_segment_def)
  show ?thesis
    unfolding closed_segment_surface[OF a  b]
    apply (rule flow_transversal_surface_finite_intersections[where Ds="λ_. blinfun_inner_left (rot (b - a))"])
    by
      (use assms in auto intro!: closed_Collect_conj closed_halfspace_component_ge closed_halfspace_component_le
        derivative_eq_intros
        simp: transversal_segment_def nrm_reverse[where x=a] in_closed_segment_iff_rot)
qed

lemma transversal_bound_posE:
  assumes transversal: "transversal_segment a b"
  assumes direction: "z  {a -- b}" "f z  (rot (a - b)) > 0"
  obtains d B where "d > 0" "0 < B"
    "x y. x  {a -- b}  dist x y  d  f y  (rot (a - b))  B"
proof -
  let ?a = "(λy. (f y)  (rot (a - b)))"
  from transversal_segment_posD[OF transversal direction]
  have seg: "a  b" "{a--b}  X" "z  {a--b}  0 < f z  rot (a - b)" for z
    by auto
  {
    fix x
    assume "x  {a--b}"
    then have "x  X" "f x  0" "a  b" using transversal by (auto simp: transversal_segment_def)
    then have "?a x ?a x"
      by (auto intro!: tendsto_eq_intros)
    moreover have "?a x > 0"
      using seg x  {a -- b} f x  0
      by (auto simp: simp del: divide_const_simps
          intro!: divide_pos_pos mult_pos_pos)
    ultimately have "F x in at x. ?a x > 0"
      by (rule order_tendstoD)
    moreover have "F x in at x. x  X"
      by (rule topological_tendstoD[OF tendsto_ident_at open_dom x  X])
    moreover have "F x in at x. f x  0"
      by (rule tendsto_imp_eventually_ne tendsto_intros x  X f x  0)+
    ultimately have "F x in at x. ?a x>0  x  X  f x  0" by eventually_elim auto
    then obtain d where d: "0 < d" "y. y  cball x d  ?a y > 0  y  X  f y  0"
      using ?a x > 0 x  X
      by (force simp: eventually_at_le dist_commute)

    have "continuous_on (cball x d) ?a"
      using d a  b
      by (auto intro!: continuous_intros)
    from compact_continuous_image[OF this compact_cball]
    have "compact (?a ` cball x d)" .
    from compact_attains_inf[OF this] obtain s where "s  cball x d" "xcball x d. ?a x  ?a s"
      using d > 0
      by auto
    then have "d>0. b>0. x  cball x d. ?a x  b"
      using d
      by (force simp: intro: exI[where x="?a s"])
  } then obtain dx Bx where dB:
    "x y. x  {a -- b}  ycball x (dx x)  ?a y  Bx x"
    "x. x  {a -- b}  Bx x > 0"
    "x. x  {a -- b}  dx x > 0"
    by metis
  define d' where "d' = (λx. dx x / 2)"
  have d':
    "x. x  {a -- b}  ycball x (d' x). ?a y  Bx x"
    "x. x  {a -- b}  d' x > 0"
    using dB(1,3) by (force simp: d'_def)+
  have d'B: "x. x  {a -- b}  ycball x (d' x). ?a y  Bx x"
    using d' by auto
  have "{a--b}  ((λx. ball x (d' x)) ` {a -- b})"
    using d'(2) by auto
  from compactE_image[OF compact_segment _ this]
  obtain X where X: "X  {a--b}"
    and [simp]: "finite X"
    and cover: "{a--b}  (xX. ball x (d' x))"
    by auto
  have [simp]: "X  {}" using X cover by auto
  define d where "d = Min (d' ` X)"
  define B where "B = Min (Bx ` X)"
  have "d > 0"
    using X d'
    by (auto simp: d_def d'_def)
  moreover have "B > 0"
    using X dB
    by (auto simp: B_def simp del: divide_const_simps)
  moreover have "B  ?a y" if "x  {a -- b}" "dist x y  d" for x y
  proof -
    from x  {a -- b} obtain xc where xc: "xc  X" "x  ball xc (d' xc)"
      using cover by auto
    have "?a y  Bx xc"
    proof (rule dB)
      show "xc  {a -- b}" using xc X  _ by auto
      have "dist xc y  dist xc x + dist x y" by norm
      also have "dist xc x  d' xc" using xc by auto
      also note dist x y  d
      also have "d  d' xc"
        using xc
        by (auto simp: d_def)
      also have "d' xc + d' xc = dx xc" by (simp add: d'_def)
      finally show "y  cball xc (dx xc)" by simp
    qed
    also have "B  Bx xc"
      using xc
      unfolding B_def
      by (auto simp: B_def)
    finally (xtrans) show ?thesis .
  qed
  ultimately show ?thesis ..
qed

lemma transversal_bound_negE:
  assumes transversal: "transversal_segment a b"
  assumes direction: "z  {a -- b}" "f z  (rot (a - b)) < 0"
  obtains d B where "d > 0" "0 < B"
    "x y. x  {a -- b}  dist x y  d  f y  (rot (b - a))  B"
proof -
  from direction have "z  {b -- a}" "f z  (rot (b - a)) > 0"
    by (auto simp: closed_segment_commute rot_diff_commute[of b a])
  from transversal_bound_posE[OF transversal_segment_reverse[OF transversal] this]
  obtain d B where "d > 0" "0 < B"
    "x y. x  {a -- b}  dist x y  d  f y  (rot (b - a))  B"
    by (auto simp: closed_segment_commute)
  then show ?thesis ..
qed

lemma leaves_transversal_segmentE:
  assumes transversal: "transversal_segment a b"
  obtains T n where "T > 0" "n = a - b  n = b - a"
    "x. x  {a -- b}  {-T..T}  existence_ivl0 x"
    "x s. x  {a -- b}  0 < s  s  T 
    (flow0 x s - x)  rot n > 0"
    "x s. x  {a -- b}  -T  s  s < 0 
    (flow0 x s - x)  rot n < 0"
proof -
  from transversal_segmentE[OF assms(1)] obtain n
    where n: "n = (a - b)  n = (b - a)"
      and seg: "a  b" "{a -- b}  X" "z. z  {a--b}  f z  rot n > 0"
    by metis
  from open_existence_ivl_on_compact[OF {a -- b}  X]
  obtain t where "0 < t" and t: "x  {a--b}  {- t..t}  existence_ivl0 x" for x
    by auto
  from n obtain d B where B: "0 < d" "0 < B" "(x y. x  {a--b}  dist x y  d  B  f y  rot n)"
  proof
    assume n_def: "n = a - b"
    with seg have pos:  "0 < f a  rot (a - b)"
      by auto
    from transversal_bound_posE[OF transversal ends_in_segment(1) pos, folded n_def]
    show ?thesis using that by blast
  next
    assume n_def: "n = b - a"
    with seg have pos:  "0 > f a  rot (a - b)"
      by (auto simp: rot_diff_commute[of a b])
    from transversal_bound_negE[OF transversal ends_in_segment(1) this, folded n_def]
    show ?thesis using that by blast
  qed
  define S where "S = ((λx. ball x d) ` {a -- b})"
  have S: "x  S  B  f x  rot n" for x
    by (auto simp: S_def intro!: B)
  have "open S" by (auto simp: S_def)
  have "{a -- b}  S"
    by (auto simp: S_def 0 < d)
  have "F (t, x) in at (0, x). flow0 x t  S" if "x  {a -- b}" for x
    unfolding split_beta'
    apply (rule topological_tendstoD tendsto_intros)+
    using set_mp[OF {a -- b}  X that] 0 < d that open S {a -- b}  S
    by force+
  then obtain d' where d':
    "x. x  {a--b}  d' x > 0"
    "x y s. x  {a--b}  (s = 0  y  x)  dist (s, y) (0, x) < d' x  flow0 y s  S"
    by (auto simp: eventually_at) metis
  define d2 where "d2 x = d' x / 2" for x
  have d2: "x. x  {a--b}  d2 x > 0" using d' by (auto simp: d2_def)
  have C: "{a--b}  ((λx. ball x (d2 x)) ` {a -- b})"
    using d2 by auto
  from compactE_image[OF compact_segment _ C]
  obtain C' where "C'  {a--b}" and [simp]: "finite C'"
    and C'_cover: "{a--b}  (cC'. ball c (d2 c))" by auto

  define T where "T = Min (insert t (d2 ` C'))"

  have "T > 0"
    using 0 < t d2 C'  _ 
    by (auto simp: T_def)
  moreover
  note n
  moreover
  have T_ex: "{-T..T}  existence_ivl0 x" if "x  {a--b}" for x
    by (rule order_trans[OF _ t[OF that]]) (auto simp: T_def)
  moreover
  have B_le: "B  f (flow0 x ξ)  rot n"
    if "x  {a -- b}"
      and c': "c'  C'" "x  ball c' (d2 c')"
      and "ξ  0" and ξ_le: "¦ξ¦ < d2 c'"
    for x c' ξ
  proof -
    have "c'  {a -- b}" using c' C'  _ by auto
    moreover have "ξ = 0  x  c'" using ξ  0 by simp
    moreover have "dist (ξ, x) (0, c') < d' c'"
    proof -
      have "dist (ξ, x) (0, c')  dist (ξ, x) (ξ, c') + dist (ξ, c') (0, c')"
        by norm
      also have "dist (ξ, x) (ξ, c') < d2 c'"
        using c'
        by (simp add: dist_prod_def dist_commute)
      also
      have "T  d2 c'" using c'
        by (auto simp: T_def)
      then have "dist (ξ, c') (0, c') < d2 c'"
        using ξ_le
        by (simp add: dist_prod_def)
      also have "d2 c' + d2 c' = d' c'" by (simp add: d2_def)
      finally show ?thesis by simp
    qed
    ultimately have "flow0 x ξ  S"
      by (rule d')
    then show ?thesis
      by (rule S)
  qed
  let ?g = "(λx t. (flow0 x t - x)  rot n)"
  have cont: "continuous_on {-T .. T} (?g x)"
    if "x  {a--b}" for x
    using T_ex that
    by (force intro!: continuous_intros)
  have deriv: "-T  s'  s'  T  ((?g x) has_derivative
      (λt. t * (f (flow0 x s')  rot n))) (at s')"
    if "x  {a--b}" for x s'
    using T_ex that
    by (force intro!: derivative_eq_intros simp: flowderiv_def blinfun.bilinear_simps)

  have "(flow0 x s - x)  rot n > 0" if "x  {a -- b}" "0 < s" "s  T" for x s
  proof (rule ccontr, unfold not_less)
    have [simp]: "x  X" using that {a -- b}  X by auto
    assume H: "(flow0 x s - x)  rot n  0"
    have cont: "continuous_on {0 .. s} (?g x)"
      using cont by (rule continuous_on_subset) (use that in auto)
    from mvt[OF 0 < s cont deriv] that
    obtain ξ where ξ: "0 < ξ" "ξ < s" "(flow0 x s - x)  rot n = s * (f (flow0 x ξ)  rot n)"
      by (auto intro: continuous_on_subset)
    note 0 < B
    also
    from C'_cover that obtain c' where c': "c'  C'" "x  ball c' (d2 c')" by auto
    have "B  f (flow0 x ξ)  rot n"
    proof (rule B_le[OF that(1) c'])
      show "ξ  0" using 0 < ξ by simp
      have "T  d2 c'" using c'
        by (auto simp: T_def)
      then show "¦ξ¦ < d2 c'"
        using 0 < ξ ξ < s s  T
        by (simp add: dist_prod_def)
    qed
    also from ξ H have "  0"
      by (auto simp add: algebra_split_simps not_less split: if_splits)
    finally show False by simp
  qed
  moreover
  have "(flow0 x s - x)  rot n < 0" if "x  {a -- b}" "-T  s" "s < 0" for x s
  proof (rule ccontr, unfold not_less)
    have [simp]: "x  X" using that {a -- b}  X by auto
    assume H: "(flow0 x s - x)  rot n  0"
    have cont: "continuous_on {s .. 0} (?g x)"
      using cont by (rule continuous_on_subset) (use that in auto)
    from mvt[OF s < 0 cont deriv] that
    obtain ξ where ξ: "s < ξ" "ξ < 0" "(flow0 x s - x)  rot n = s * (f (flow0 x ξ)  rot n)"
      by auto
    note 0 < B
    also
    from C'_cover that obtain c' where c': "c'  C'" "x  ball c' (d2 c')" by auto
    have "B  (f (flow0 x ξ)  rot n)"
    proof (rule B_le[OF that(1) c'])
      show "ξ  0" using 0 > ξ by simp
      have "T  d2 c'" using c'
        by (auto simp: T_def)
      then show "¦ξ¦ < d2 c'"
        using 0 > ξ ξ > s s  - T
        by (simp add: dist_prod_def)
    qed
    also from ξ H have "  0"
      by (simp add: algebra_split_simps)
    finally show False by simp
  qed
  ultimately show ?thesis ..
qed


lemma inner_rot_pos_move_base: "(x - a)  rot (a - b) > 0"
  if "(x - y)  rot (a - b) > 0" "y  {a -- b}"
  by (smt in_segment_inner_rot inner_diff_left inner_minus_right minus_diff_eq rot_rot that)

lemma inner_rot_neg_move_base: "(x - a)  rot (a - b) < 0"
  if "(x - y)  rot (a - b) < 0" "y  {a -- b}"
  by (smt in_segment_inner_rot inner_diff_left inner_minus_right minus_diff_eq rot_rot that)

lemma inner_pos_move_base: "(x - a)  n > 0"
  if "(a - b)  n = 0" "(x - y)  n > 0" "y  {a -- b}"
proof -
  from that(3) obtain u where y_def: "y = (1 - u) *R a + u *R b" and u: "0  u" "u  1"
    by (auto simp: in_segment)
  have "(x - a)  n = (x - y)  n - u * ((a - b)  n)"
    by (simp add: algebra_simps y_def)
  also have " = (x - y)  n"
    by (simp add: that)
  also note  > 0
  finally show ?thesis .
qed

lemma inner_neg_move_base: "(x - a)  n < 0"
  if "(a - b)  n = 0" "(x - y)  n < 0" "y  {a -- b}"
proof -
  from that(3) obtain u where y_def: "y = (1 - u) *R a + u *R b" and u: "0  u" "u  1"
    by (auto simp: in_segment)
  have "(x - a)  n = (x - y)  n - u * ((a - b)  n)"
    by (simp add: algebra_simps y_def)
  also have " = (x - y)  n"
    by (simp add: that)
  also note  < 0
  finally show ?thesis .
qed

lemma rot_same_dir:
  assumes "x1  {a<--<b}"
  assumes "x2  {x1<--<b}"
  shows "(y  rot (a-b) > 0) = (y  rot(x1-x2) > 0)"  "(y  rot (a-b) < 0) = (y  rot(x1-x2) < 0)"
  using oriented_subsegment_scale[OF assms]
   apply (smt inner_scaleR_right nrm_reverse rot_scaleR zero_less_mult_iff)
  by (smt thesis. (e. 0 < e; b - a = e *R (x2 - x1)  thesis)  thesis inner_minus_right inner_scaleR_right rot_diff_commute rot_scaleR zero_less_mult_iff)


subsection ‹Monotone Step Lemma›

lemma flow0_transversal_segment_monotone_step:
  assumes "transversal_segment a b"
  assumes "t1  t2" "{t1..t2}  existence_ivl0 x"
  assumes x1: "flow0 x t1  {a<--<b}"
  assumes x2: "flow0 x t2  {flow0 x t1<--<b}"
  assumes "t. t  {t1<..<t2}  flow0 x t  {a<--<b}"
  assumes "t > t2" "t  existence_ivl0 x"
  shows "flow0 x t  {a<--<flow0 x t2}"
proof -
  note exist = {t1..t2}  existence_ivl0 x
  note t1t2 = t. t  {t1<..<t2}  flow0 x t  {a<--<b}
    (* Basic properties of the segment *)
  have x1neqx2: "flow0 x t1  flow0 x t2"
    using open_segment_def x2 by force 
  then have t1neqt2: "t1  t2" by auto

  have [simp]: "a  b" and {a -- b}  X using transversal_segment a b
    by (auto simp: transversal_segment_def)

  from x1 obtain i1 where i1: "flow0 x t1 = line a b i1" "0 < i1" "i1 < 1"
    by (auto simp: in_open_segment_iff_line)
  from x2 obtain i2 where i2: "flow0 x t2 = line a b i2" "0 < i1" "i1 < i2"
    by (auto simp: i1 line_open_segment_iff)


  have "{a <--< flow0 x t1}  {a<--<b}"
    by (simp add: open_closed_segment subset_open_segment x1) 
  have t12sub: "{flow0 x t1--flow0 x t2}  {a<--<b}"
    by (metis ends_in_segment(2) open_closed_segment subset_co_segment subset_eq subset_open_segment x1 x2)
  have subr: "{flow0 x t1<--<flow0 x t2}  {flow0 x t1 <--<b}"
    by (simp add: open_closed_segment subset_open_segment x2)
  have "flow0 x t1  {a <--<flow0 x t2}" using x1 x2
    by (rule open_segment_subsegment)
  then have subl: "{flow0 x t1<--<flow0 x t2}  {a <--< flow0 x t2}" using x1 x2
    by (simp add: open_closed_segment subset_open_segment x2)
  then have subl2: "{flow0 x t1--<flow0 x t2}  {a <--< flow0 x t2}" using x1 x2
    by (smt DiffE DiffI flow0 x t1  {a<--<flow0 x t2} half_open_segment_def insert_iff open_segment_def subset_eq)

  have sub1b: "{flow0 x t1--b}  {a--b}"
    by (simp add: open_closed_segment subset_closed_segment x1)
  have suba2: "{a--flow0 x t2}  {a -- b}"
    using open_closed_segment subset_closed_segment t12sub by blast
  then have suba2o: "{a<--<flow0 x t2}  {a -- b}"
    using open_closed_segment subset_closed_segment t12sub by blast
  have x2_notmem: "flow0 x t2  {a--flow0 x t1}"
    using i1 i2
    by (auto simp: closed_segment_line_iff)
  have suba12: "{a--flow0 x t1}  {a--flow0 x t2}"
    by (simp add: flow0 x t1  {a<--<flow0 x t2} open_closed_segment subset_closed_segment)
  then have suba12_open: "{a<--<flow0 x t1}  {a<--<flow0 x t2}"
    using x2_notmem
    by (auto simp: open_segment_def)
  have "flow0 x t2  {a--b}"
    using suba2 by auto

  have intereq: "t. t1  t  t  t2  flow0 x t  {a<--<b}   t = t1  t = t2"
  proof (rule ccontr)
    fix t
    assume t: "t1  t" "t  t2" "flow0 x t  {a<--<b}" "¬(t= t1  t = t2)"
    then have "t  {t1<..<t2}" by auto
    then have "flow0 x t  {a<--<b}" using t1t2 by blast
    thus False using t by auto
  qed
  then have intereqt12: "t. t1  t  t  t2  flow0 x t  {flow0 x t1--flow0 x t2}   t = t1  t = t2"
    using t12sub by blast

(* The Jordan curve *)
  define J1 where "J1 = flow_to_path x t1 t2"
  define J2 where "J2 = linepath (flow0 x t2) (flow0 x t1)" 
  define J where "J = J1 +++ J2"
    (* Proof that J is a Jordan curve *)
  have "pathfinish J = pathstart J" unfolding J_def J1_def J2_def
    by (auto simp add: pathstart_compose pathfinish_compose)
  have piJ: "path_image J = path_image J1  path_image J2"
    unfolding J_def J1_def J2_def
    apply (rule path_image_join)
    by auto
  have "flow0 x t1  flow0 x ` {t1..t2}  flow0 x t2  flow0 x ` {t1..t2}"
    using atLeastAtMost_iff t1  t2 by blast 
  then have piD: "path_image J = path_image J1  {flow0 x t1 <--<flow0 x t2}"
    unfolding piJ J1_def J2_def path_image_flow_to_path[OF t1  t2]
      path_image_linepath open_segment_def
    by (smt Diff_idemp Diff_insert2 Un_Diff_cancel closed_segment_commute mk_disjoint_insert)
  have "s{t1<..<t2}. flow0 x s  flow0 x t1"
    using x1 t1t2 by fastforce
  from flow_to_path_arc[OF t1  t2 exist this x1neqx2]
  have "arc J1" using J1_def assms flow_to_path_arc by auto
  then have "simple_path J" unfolding J_def
    using arc J1 J1_def J2_def assms x1neqx2 t1neqt2 apply (auto intro!:simple_path_join_loop)
    using intereqt12 closed_segment_commute by blast

  from Jordan_inside_outside_R2[OF this pathfinish J = pathstart J]
  obtain inner outer where inner_def: "inner = inside (path_image J)"
    and outer_def: "outer = outside (path_image J)"
    and io:
    "inner  {}" "open inner" "connected inner"
    "outer  {}" "open outer" "connected outer"
    "bounded inner" "¬ bounded outer" "inner  outer = {}"
    "inner  outer = - path_image J"
    "frontier inner = path_image J"
    "frontier outer = path_image J" by metis
  from io have io2: "outer  inner = {}" "outer  inner = - path_image J" by auto

  have swap_side: "y t. y  side2 
    0  t  t  existence_ivl0 y 
    flow0 y t  closure side1 
    T. 0 < T  T  t  (s {0..<T}. flow0 y s  side2) 
        flow0 y T  {flow0 x t1--<flow0 x t2}"
    if "side1  side2 = {}"
      "open side2"
      "frontier side1 = path_image J"
      "frontier side2 = path_image J"
      "side1  side2 = - path_image J"
    for side1 side2
  proof -
    fix y t
    assume yt: "y  side2" "0  t" "t  existence_ivl0 y"
      "flow0 y t  closure side1"
    define fp where "fp = flow_to_path y 0 t"
    have ex:"{0..t}  existence_ivl0 y"
      using ivl_subset_existence_ivl yt(3) by blast
    then have y0:"flow0 y 0 = y"
      using mem_existence_ivl_iv_defined(2) yt(3) by auto
    then have tpos: "t > 0" using yt(2)  side1  side2 = {}
      using yt(1) yt(4)
      by (metis closure_iff_nhds_not_empty less_eq_real_def order_refl that(2)) 
    from flow_to_path_path[OF yt(2) ex]
    have a1: "path fp" unfolding fp_def .
    have "y  closure side2" using yt(1)
      by (simp add: assms closure_def)
    then have a2: "pathstart fp  closure side2" unfolding fp_def using y0 by auto
    have a3:"pathfinish fp  side2" using yt(4) side1  side2 = {}
      unfolding fp_def apply auto
      using closure_iff_nhds_not_empty that(2) by blast
    from subpath_to_frontier_strong[OF a1 a3]
    obtain u where u:"0  u" "u  1"
      "fp u  interior side2"
      "u = 0 
      (x. 0  x  x < 1 
        subpath 0 u fp x  interior side2)  fp u  closure side2" by blast
    have p1:"path_image (subpath 0 u fp) =  flow0 y ` {0 ..  u*t}"
      unfolding fp_def subpath0_flow_to_path using path_image_flow_to_path
      by (simp add: u(1) yt(2))
    have p2:"fp u = flow0 y (u*t)" unfolding fp_def flow_to_path_unfold by simp
    have inout:"interior side2 = side2" using open side2
      by (simp add: interior_eq)
    then have iemp: "side2  path_image J = {}"
      using frontier side2 = path_image J
      by (metis frontier_disjoint_eq inf_sup_aci(1) interior_eq)
    have "u  0" using inout u(3) y0 p2 yt(1) by force
    then have c1:"u * t > 0" using tpos u y0  side1  side2 = {}
      using frontier_disjoint_eq io(5) yt(1) zero_less_mult_iff by fastforce
    have uim:"fp u  path_image J" using u u  0
      using frontier side2 = path_image J
      by (metis ComplI IntI closure_subset frontier_closures inout subsetD) 
    have c2:"u * t  t"  using u(1-2) tpos by auto
    have"(flow_to_path y 0 (u * t) ` {0..<1}  side2)"
      using u  0 u inout unfolding fp_def subpath0_flow_to_path by auto
    then have c3:"s {0..<u*t}. flow0 y s  side2" by auto
    have c4: "flow0 y (u*t)  path_image J"
      using uim path_image_join_subset
      by (simp add: p2)
    have "flow0 y (u*t)  path_image J1  flow0 y (u*t) = flow0 x t1"
    proof clarsimp
      assume "flow0 y (u*t)  path_image J1"
      then obtain s where s: "t1  s" "s  t2" "flow0 x s = flow0 y (u*t)"
        using J1_def t1  t2 by auto
      have "s = t1"
      proof (rule ccontr)
        assume "s  t1"
        then have st1:"s > t1" using s(1) by linarith
        define sc where "sc = min (s-t1) (u*t)"
        have scd: "s-sc  {t1..t2}" unfolding sc_def
          using c1 s(1) s(2) by auto
        then have *:"flow0 x (s-sc)  path_image J1" unfolding J1_def path_image_flow_to_path[OF t1  t2]
          by blast
        have "flow0 x (s-sc) = flow0 (flow0 x s) (-sc)"
          by (smt exist atLeastAtMost_iff existence_ivl_trans' flow_trans s(1) s(2) scd subsetD)
        then have **:"flow0 (flow0 y (u*t)) (-sc)   path_image J1"
          using s(3) * by auto
        have b:"u*t - sc  {0..<u*t}" unfolding sc_def by (simp add: st1 c1 s(1))
        then have "u*t - sc  existence_ivl0 y"
          using c2 ex by auto 
        then have "flow0 y (u*t - sc)  path_image J1" using **
          by (smt atLeastAtMost_iff diff_existence_ivl_trans ex flow_trans mult_left_le_one_le mult_nonneg_nonneg subset_eq u(1) u(2) yt(2))
        thus False using b c3 iemp piJ by blast
      qed
      thus "flow0 y (u * t) = flow0 x t1" using s by simp
    qed
    thus "T>0. T  t  (s{0..<T}. flow0 y s  side2) 
          flow0 y T  {flow0 x t1--<flow0 x t2}"
      using c1 c2 c3 c4 unfolding piD
      by (metis DiffE UnE ends_in_segment(1) half_open_segment_closed_segmentI insertCI open_segment_def x1neqx2)
  qed
  have outside_in: "y t. y  outer 
    0  t  t  existence_ivl0 y 
    flow0 y t  closure inner 
    T. 0 < T  T  t  (s {0..<T}. flow0 y s  outer) 
          flow0 y T  {flow0 x t1--<flow0 x t2}"
    by (rule swap_side; (rule io | assumption))
  have inside_out: "y t. y  inner 
    0  t  t  existence_ivl0 y 
    flow0 y t  closure outer 
    T. 0 < T  T  t  (s {0..<T}. flow0 y s  inner) 
          flow0 y T  {flow0 x t1--<flow0 x t2}"
    by (rule swap_side; (rule io2 io | assumption))

  from leaves_transversal_segmentE[OF assms(1)]
  obtain d n where d: "d > (0::real)"
    and n: "n = a - b  n = b - a"
    and d_ex: "x. x  {a -- b}  {-d..d}  existence_ivl0 x"
    and d_above: "x s. x  {a -- b}  0 < s  s  d  (flow0 x s - x)  rot n > 0"
    and d_below: "x s. x  {a -- b}  -d  s  s < 0  (flow0 x s - x)  rot n < 0"
    by blast

  have ortho: "(a - b)  rot n = 0"
    using n by (auto simp: algebra_simps)

(* These "rectangles" are either fully inside or fully outside
           |-----------------------|
           |           r1          | (flow d)
    a --- (t1) --- rp --- (t2) --- b
    |          r2           | (flow -d)
    |-----------------------|
   *)
  define r1 where "r1 = (λ(x, y). flow0 x y)`({flow0 x t1<--<b} × {0<..<d}) "
  have r1a1: "path_connected {flow0 x t1 <--<b}" by simp
  have r1a2: "path_connected {0<..<d}" by simp
  have "{flow0 x t1<--<b}  {a--b}"
    by (simp add: open_closed_segment subset_oc_segment x1)
  then have r1a3: "y  {flow0 x t1<--<b}  {0<..<d}  existence_ivl0 y" for y
    using d_ex[of y]
    by force
  from flow0_path_connected[OF r1a1 r1a2 r1a3]
  have pcr1:"path_connected r1" unfolding r1_def by auto
  have pir1J1: "r1  path_image J1 = {}"
    unfolding J1_def path_image_flow_to_path[OF t1  t2]
  proof (rule ccontr)
    assume "r1  flow0 x ` {t1..t2}  {}"
    then obtain xx tt ss where
      eq: "flow0 xx tt = flow0 x ss"
      and xx: "xx  {flow0 x t1<--<b}"
      and ss: "t1  ss" "ss  t2"
      and tt: "0 < tt" "tt < d"
      unfolding r1_def
      by force
    have "xx  {a -- b}"
      using sub1b
      apply (rule set_mp)
      using xx by (simp add: open_closed_segment)
    then have [simp]: "xx  X" using transversal_segment a b by (auto simp: transversal_segment_def)
    from ss have ss_ex: "ss  existence_ivl0 x" using exist
      by auto
    from d_ex[OF xx  {a -- b}] tt
    have tt_ex: "tt  existence_ivl0 xx" by auto
    then have neg_tt_ex: "- tt  existence_ivl0 (flow0 xx tt)"
      by (rule existence_ivl_reverse[simplified])
    from eq have "flow0 (flow0 xx tt) (-tt) = flow0 (flow0 x ss) (-tt)"
      by simp
    then have "xx = flow0 x (ss - tt)"
      apply (subst (asm) flow_trans[symmetric])
        apply (rule tt_ex)
       apply (rule neg_tt_ex)
      apply (subst (asm) flow_trans[symmetric])
        apply (rule ss_ex)
       apply (subst eq[symmetric])
       apply (rule neg_tt_ex)
      by simp
    moreover
    define e where "e = ss - t1"
    consider "e > tt" | "e  tt" by arith
    then show False
    proof cases
      case 1
      have "flow0 (flow0 x ss) (-tt)  {a<--<b}"
        apply (subst flow_trans[symmetric])
          apply fact
        subgoal using neg_tt_ex eq by simp
        apply (rule t1t2)
        using 1 ss tt
        unfolding e_def
        by auto
      moreover have "flow0 (flow0 x ss) (-tt)  {a<--<b}"
        unfolding eq[symmetric] using tt_ex xx
        apply (subst flow_trans[symmetric])
          apply (auto simp add: neg_tt_ex)
        by (metis (no_types, opaque_lifting) sub1b subset_eq subset_open_segment)
      ultimately show ?thesis by simp
    next
      case 2
      have les: "0  tt - e" "tt - e  d"
        using tt ss 2 e_def
        by auto
      have xxtte: "flow0 xx (tt - e) = flow0 x t1"
        apply (simp add: e_def)
        by (smt 0  tt - e {- d..d}  existence_ivl0 xx atLeastAtMost_iff e_def eq
            local.existence_ivl_reverse local.existence_ivl_trans local.flow_trans ss(1) ss_ex subset_iff tt(2))
      show False
      proof (cases "tt = e")
        case True
        with xxtte have "xx = flow0 x t1"
          by simp
        with xx show ?thesis
          apply auto
          by (auto simp: open_segment_def)
      next
        case False
        with les have "0 < tt - e" by (simp)
        from d_above[OF xx  {a -- b} this tt - e  d]
        have "flow0 xx (tt - e)  {a -- b}"
          apply (simp add: in_closed_segment_iff_rot[OF a  b]
              not_le )
          by (smt xx  {a--b} inner_minus_right inner_rot_neg_move_base inner_rot_pos_move_base n rot_diff_commute)
        with xxtte show ?thesis
          using flow0 x t1  {a<--<flow0 x t2} suba2o by auto
      qed
    qed
  qed
    (* for sufficiently small d, the flow does not return to the line *)
  moreover
  have pir1J2: "r1  path_image J2 = {}"
  proof -
    have "r1  {x. (x - a)  rot n > 0}"
      unfolding r1_def
    proof safe
      fix aa ba
      assume "aa  {flow0 x t1<--<b}" "ba  {0<..<d}"
      with sub1b show "0 < (flow0 aa ba - a)  rot n"
        using segment_open_subset_closed[of "flow0 x t1" b]
        by (intro inner_pos_move_base[OF ortho d_above]) auto
    qed
    also have "  {a -- b} = {}"
      using in_segment_inner_rot in_segment_inner_rot2 n by auto
    finally show ?thesis
      unfolding J2_def path_image_linepath
      using t12sub open_closed_segment
      by (force simp: closed_segment_commute)
  qed
  ultimately have pir1:"r1  (path_image J) = {}" unfolding J_def
    by (metis disjoint_iff_not_equal not_in_path_image_join)

  define r2 where "r2 =(λ(x, y). flow0 x y)`({a <--< flow0 x t2} × {-d<..<0})"
  have r2a1:"path_connected {a <--< flow0 x t2}" by simp
  have r2a2:"path_connected {-d<..<0}" by simp
  have "{a <--< flow0 x t2}  {a -- b}"
    by (meson ends_in_segment(1) open_closed_segment subset_co_segment subset_oc_segment t12sub)
  then have r2a3: "y  {a <--< flow0 x t2}  {-d<..<0}  existence_ivl0 y" for y
    using d_ex[of y]
    by force
  from flow0_path_connected[OF r2a1 r2a2 r2a3]
  have pcr2:"path_connected r2" unfolding r2_def by auto
  have pir2J2: "r2  path_image J1 = {}"
    unfolding J1_def path_image_flow_to_path[OF t1  t2]
  proof (rule ccontr)
    assume "r2  flow0 x ` {t1..t2}  {}"
    then obtain xx tt ss where
      eq: "flow0 xx tt = flow0 x ss"
      and xx: "xx  {a<--<flow0 x t2}"
      and ss: "t1  ss" "ss  t2"
      and tt: "-d < tt" "tt < 0"
      unfolding r2_def
      by force
    have "xx  {a -- b}"
      using suba2
      apply (rule set_mp)
      using xx by (simp add: open_closed_segment)
    then have [simp]: "xx  X" using transversal_segment a b by (auto simp: transversal_segment_def)
    from ss have ss_ex: "ss  existence_ivl0 x" using exist
      by auto
    from d_ex[OF xx  {a -- b}] tt
    have tt_ex: "tt  existence_ivl0 xx" by auto
    then have neg_tt_ex: "- tt  existence_ivl0 (flow0 xx tt)"
      by (rule existence_ivl_reverse[simplified])
    from eq have "flow0 (flow0 xx tt) (-tt) = flow0 (flow0 x ss) (-tt)"
      by simp
    then have "xx = flow0 x (ss - tt)"
      apply (subst (asm) flow_trans[symmetric])
        apply (rule tt_ex)
       apply (rule neg_tt_ex)
      apply (subst (asm) flow_trans[symmetric])
        apply (rule ss_ex)
       apply (subst eq[symmetric])
       apply (rule neg_tt_ex)
      by simp
    moreover
    define e where "e = t2 - ss"
    consider "e > - tt" | "e  -tt" by arith
    then show False
    proof cases
      case 1
      have "flow0 (flow0 x ss) (-tt)  {a<--<b}"
        apply (subst flow_trans[symmetric])
          apply fact
        subgoal using neg_tt_ex eq by simp
        apply (rule t1t2)
        using 1 ss tt
        unfolding e_def
        by auto
      moreover have "flow0 (flow0 x ss) (-tt)  {a<--<b}"
        unfolding eq[symmetric] using tt_ex xx
        apply (subst flow_trans[symmetric])
          apply (auto simp add: neg_tt_ex)
        by (metis (no_types, opaque_lifting) suba2 subset_eq subset_open_segment)
      ultimately show ?thesis by simp
    next
      case 2
      have les: "tt + e  0" "-d  tt + e"
        using tt ss 2 e_def
        by auto
      have xxtte: "flow0 xx (tt + e) = flow0 x t2"
        apply (simp add: e_def)
        by (smt atLeastAtMost_iff calculation eq exist local.existence_ivl_trans' local.flow_trans neg_tt_ex ss_ex subset_iff t1  t2)
      show False
      proof (cases "tt=-e")
        case True
        with xxtte have "xx = flow0 x t2"
          by simp
        with xx show ?thesis
          apply auto
          by (auto simp: open_segment_def)
      next
        case False
        with les have "tt+e < 0" by simp
        from d_below[OF xx  {a -- b}  -d  tt + e this]
        have "flow0 xx (tt + e)  {a -- b}"
          apply (simp add: in_closed_segment_iff_rot[OF a  b]
              not_le )
          by (smt xx  {a--b} inner_minus_right inner_rot_neg_move_base inner_rot_pos_move_base n rot_diff_commute)
        with xxtte show ?thesis
          using flow0 x t2  {a--b} by simp
      qed
    qed
  qed
  moreover
  have pir2J2: "r2  path_image J2 = {}"
  proof -
    have "r2  {x. (x - a)  rot n < 0}"
      unfolding r2_def
    proof safe
      fix aa ba
      assume "aa  {a<--<flow0 x t2}" "ba  {-d<..<0}"
      with suba2 show "0 > (flow0 aa ba - a)  rot n"
        using segment_open_subset_closed[of a "flow0 x t2"]
        by (intro inner_neg_move_base[OF ortho d_below]) auto
    qed
    also have "  {a -- b} = {}"
      using in_segment_inner_rot in_segment_inner_rot2 n by auto
    finally show ?thesis
      unfolding J2_def path_image_linepath
      using t12sub open_closed_segment
      by (force simp: closed_segment_commute)
  qed
  ultimately have pir2:"r2  (path_image J) = {}"
    unfolding J_def
    by (metis disjoint_iff_not_equal not_in_path_image_join)

  define rp where "rp = midpoint (flow0 x t1) (flow0 x t2)"
  have rpi: "rp  {flow0 x t1<--<flow0 x t2}" unfolding rp_def
    by (simp add: x1neqx2)
  have "rp  {a -- b}"
    using rpi suba2o subl by blast
  then have [simp]: "rp  X"
    using {a--b}  X by blast

(* The fundamental case distinction *)
  have *: "pathfinish J1 = flow0 x t2"
    "pathstart J1 = flow0 x t1"
    "rp  {flow0 x t2<--<flow0 x t1}"
    using rpi
    by (auto simp: open_segment_commute J1_def)
  have "{y. 0 < (y - flow0 x t2)  rot (flow0 x t2 - flow0 x t1)} = {y. 0 < (y - rp)  rot (flow0 x t2 - flow0 x t1)}"
    by (smt Collect_cong in_open_segment_rotD inner_diff_left nrm_dot rpi)
  also have "... =  {y. 0 > (y - rp)  rot (flow0 x t1 - flow0 x t2)}"
    by (smt Collect_cong inner_minus_left nrm_reverse)
  also have " ... = {y. 0 > (y - rp)  rot (a - b) }"
    by (metis rot_same_dir(2) x1 x2)
  finally have side1: "{y. 0 < (y - flow0 x t2)  rot (flow0 x t2 - flow0 x t1)} = {y. 0 > (y - rp)  rot (a - b) }"
    (is "_ = ?lower1") .
  have "{y. (y - flow0 x t2)  rot (flow0 x t2 - flow0 x t1) < 0} = {y. (y - rp)  rot (flow0 x t2 - flow0 x t1) < 0}"
    by (smt Collect_cong in_open_segment_rotD inner_diff_left nrm_dot rpi)
  also have "... =  {y. (y - rp)  rot (flow0 x t1 - flow0 x t2) > 0}"
    by (smt Collect_cong inner_minus_left nrm_reverse)
  also have " ... = {y. 0 < (y - rp)  rot (a - b) }"
    by (metis rot_same_dir(1) x1 x2)
  finally have side2: "{y. (y - flow0 x t2)  rot (flow0 x t2 - flow0 x t1) < 0} = {y. 0 < (y - rp)  rot (a - b) }"
    (is "_ = ?upper1") .
  from linepath_ball_inside_outside[OF simple_path J[unfolded J_def J2_def] *,
      folded J2_def J_def, unfolded side1 side2]
  obtain e where e0: "0 < e"
    "ball rp e  path_image J1 = {}"
    "ball rp e  ?lower1  inner 
        ball rp e  ?upper1  outer 
        ball rp e  ?upper1  inner 
        ball rp e  ?lower1  outer"
    by (auto simp: inner_def outer_def)

  let ?lower = "{y. 0 > (y - rp)  rot n }"
  let ?upper = "{y. 0 < (y - rp)  rot n }"
  have "?lower1 = {y. 0 < (y - rp)  rot n }  ?upper1 = {y. 0 > (y - rp)  rot n } 
      ?lower1 = {y. 0 > (y - rp)  rot n }  ?upper1 =  {y. 0 < (y - rp)  rot n }"
    using n rot_diff_commute[of a b]
    by auto
  from this e0 have e: "0 < e"
    "ball rp e  path_image J1 = {}"
    "ball rp e  ?lower  inner 
        ball rp e  ?upper  outer 
        ball rp e  ?upper  inner 
        ball rp e  ?lower  outer"
    by auto

  have "F t in at_right 0. t < d"
    by (auto intro!: order_tendstoD 0 < d)
  then have evr: "F t in at_right 0. 0 < (flow0 rp t - rp)  rot n"
    unfolding eventually_at_filter
    by eventually_elim (auto intro!: rp  {a--b} d_above)
  have "F t in at_left 0. t > -d"
    by (auto intro!: order_tendstoD 0 < d)
  then have evl: "F t in at_left 0. 0 > (flow0 rp t - rp)  rot n"
    unfolding eventually_at_filter
    by eventually_elim (auto intro!: rp  {a--b} d_below)
  have "F t in at 0. flow0 rp t  ball rp e"
    unfolding mem_ball
    apply (subst dist_commute)
    apply (rule tendstoD)
    by (auto intro!: tendsto_eq_intros 0 < e)
  then have evl2: "(F t in at_left 0. flow0 rp t  ball rp e)"
    and evr2: "(F t in at_right 0. flow0 rp t  ball rp e)"
    unfolding eventually_at_split by auto
  have evl3: "(F t in at_left 0. t > -d)"
    and evr3: "(F t in at_right 0. t < d)"
    by (auto intro!: order_tendstoD 0 < d)
  have evl4: "(F t in at_left 0. t < 0)"
    and evr4: "(F t in at_right 0. t > 0)"
    by (auto simp: eventually_at_filter)
  from evl evl2 evl3 evl4
  have "F t in at_left 0. (flow0 rp t - rp)  rot n < 0  flow0 rp t  ball rp e  t > -d  t < 0"
    by eventually_elim auto
  from eventually_happens[OF this]
  obtain dl where dl: "(flow0 rp dl - rp)  rot n < 0" "flow0 rp dl  ball rp e" "- d < dl" "dl < 0"
    by auto
  from evr evr2 evr3 evr4
  have "F t in at_right 0. (flow0 rp t - rp)  rot n > 0  flow0 rp t  ball rp e  t < d  t > 0"
    by eventually_elim auto
  from eventually_happens[OF this]
  obtain dr where dr: "(flow0 rp dr - rp)  rot n > 0" "flow0 rp dr  ball rp e" "d > dr" "dr > 0"
    by auto

  have "rp  {flow0 x t1<--<b}" using rpi subr by auto
  then have rpr1:"flow0 rp (dr)  r1" unfolding r1_def using d > dr dr > 0
    by auto
  have "rp  {a<--<flow0 x t2}" using rpi subl by auto
  then have rpr2:"flow0 rp (dl)  r2" unfolding r2_def using -d < dl dl < 0
    by auto

  from e(3) dr dl
  have "flow0 rp (dr)  outer  flow0 rp (dl)  inner  flow0 rp (dr)  inner  flow0 rp (dl)  outer"
    by auto
  moreover {
    assume "flow0 rp dr  outer" "flow0 rp dl  inner"
    then have
      r1o: "r1  outer  {}" and
      r2i: "r2  inner  {}" using rpr1 rpr2 by auto
    from path_connected_not_frontier_subset[OF pcr1 r1o]
    have "r1  outer" using pir1 by (simp add: io(12))
    from path_connected_not_frontier_subset[OF pcr2 r2i]
    have "r2  inner" using pir2 by (simp add: io(11))
    have "(λ(x, y). flow0 x y)`({flow0 x t2} × {0<..<d})  r1" unfolding r1_def
      by (auto intro!:image_mono simp add: x2)
    then have *:"t. 0 < t  t < d  flow0 (flow0 x t2) t  outer"
      by (smt r1  outer greaterThanLessThan_iff mem_Sigma_iff pair_imageI r1_def subset_eq x2)

    then have t2o: "t. 0 < t  t < d  flow0 x (t2 + t)  outer"
      using r1a3[OF x2] exist flow_trans
      by (metis (no_types, opaque_lifting) closed_segment_commute ends_in_segment(1) local.existence_ivl_trans' local.flow_undefined0 real_Icc_closed_segment subset_eq t1  t2)

(* Construct a sequence of times converging to these points in r2 ⊆ inner *)
    have inner: "{a <--< flow0 x t2}  closure inner"
    proof (rule subsetI)
      fix y
      assume y: "y  {a <--< flow0 x t2}"
      have [simp]: "y  X"
        using y suba12_open suba2o {a -- b}  X
        by auto
      have "(n. flow0 y (- d / real (Suc (Suc n)))  inner)"
        using y
        using suba12_open 0 < d suba2o {a -- b}  X
        by (auto intro!: set_mp[OF r2  inner] image_eqI[where x="(y, -d/Suc (Suc n))" for n]
            simp: r2_def divide_simps) 
      moreover
      have d_over_0: "(λs. - d / real (Suc (Suc s)))  0"
        by (rule real_tendsto_divide_at_top)
          (auto intro!: filterlim_tendsto_add_at_top filterlim_real_sequentially)
      have "(λn. flow0 y (- d / real (Suc (Suc n))))  y"
        apply (rule tendsto_eq_intros)
           apply (rule tendsto_intros)
          apply (rule d_over_0)
        by auto
      ultimately show "y  closure inner"
        unfolding closure_sequential
        by (intro exI[where x="λn. flow0 y (-d/Suc (Suc n))"]) (rule conjI)
    qed
    then have "{a <--< flow0 x t1}  closure inner"
      using suba12_open by blast
    then have "{flow0 x t1 -- flow0 x t2}  closure inner"
      by (metis (no_types, lifting) closure_closure closure_mono closure_open_segment dual_order.trans inner subl x1neqx2)
    have outer:"t. t > t2  t  existence_ivl0 x  flow0 x t  outer"
    proof (rule ccontr)
      fix t
      assume t: "t > t2" "t  existence_ivl0 x" "flow0 x t  outer"
      have "0  t- (t2+d)" using t2o t  by smt 
      then have a2:"0  t - (t2+dr)" using d 0 < dr dr < d by linarith
      have t2d2_ex: "t2 + dr  existence_ivl0 x"
        using t1  t2 exist d_ex[of "flow0 x t2"] flow0 x t2  {a--b} 0 < d 0 < dr dr < d 
        by (intro existence_ivl_trans) auto
      then have a3: "t - (t2 + dr)  existence_ivl0 (flow0 x (t2 + dr))"
        using t(2)
        by (intro diff_existence_ivl_trans) auto
      then have "flow0 (flow0 x (t2 + dr)) (t - (t2 + dr)) = flow0 x t"
        by (subst flow_trans[symmetric]) (auto simp: t2d2_ex)
      moreover have "flow0 x t  closure inner" using t(3) io
        by (metis ComplI Un_iff closure_Un_frontier)
      ultimately have a4: "flow0 (flow0 x (t2 + dr)) (t - (t2 + dr))  closure inner" by auto
      have a1: "flow0 x (t2+dr)  outer"
        by (simp add: d t2o 0 < dr dr < d)
      from outside_in[OF a1 a2 a3 a4]
      obtain T where T: "T > 0" "T  t - (t2 + dr)"
        "(s{0..<T}. flow0 (flow0 x (t2 + dr)) s  outer)"
        "flow0 (flow0 x (t2 + dr)) T  {flow0 x t1 --< flow0 x t2}" by blast
      define y where "y = flow0 (flow0 x (t2 + dr)) T"
      have "y  {a <--< flow0 x t2}" unfolding y_def using T(4)
        using subl2 by blast 
      then have "(λ(x, y). flow0 x y)`({y} × {-d<..<0})  r2" unfolding r2_def
        by (auto intro!:image_mono)
      then have *:"t. -d < t  t < 0  flow0 y t  r2"
        by (simp add: pair_imageI subsetD)
      have "max (-T/2) dl < 0" using d T 0 > dl dl > -d by auto
      moreover have "-d < max (-T/2) dl" using d T 0 > dl dl > -d by auto
      ultimately have inner: "flow0 y (max (-T/2) dl)  inner" using * r2  inner by blast 
      have "0(T+(max (-T/2) dl))" using T(1) by linarith
      moreover have "(T+(max (-T/2) dl)) < T" using T(1) d 0 > dl dl > -d by linarith
      ultimately have outer: " flow0 (flow0 x (t2 + dr)) (T+(max (-T/2) dl))  outer"
        using T by auto
      have T_ex: "T  existence_ivl0 (flow0 x (t2 + dr))"
        apply (subst flow_trans)
        using exist t1  t2
        using d_ex[of "flow0 x t2"] flow0 x t2  {a -- b} d > 0 T 0 < dr dr < d
          apply auto
        apply (rule set_rev_mp[where A="{0 .. t - (t2 + dr)}"], force)
        apply (rule ivl_subset_existence_ivl)
        apply (rule existence_ivl_trans')
         apply (rule existence_ivl_trans')
        by (auto simp: t)
      have T_ex2: "dr + T  existence_ivl0 (flow0 x t2)"
        by (smt T_ex ends_in_segment(2) exist local.existence_ivl_trans local.existence_ivl_trans' real_Icc_closed_segment subset_eq t2d2_ex t1  t2)
      thus False using T t1  t2 exist
        by (smt T_ex diff_existence_ivl_trans disjoint_iff_not_equal inner io(9) local.flow_trans local.flow_undefined0 outer y_def)
    qed
    have "closure inner  outer = {}"
      by (simp add: inf_sup_aci(1) io(5) io(9) open_Int_closure_eq_empty) 
    then have "flow0 x t  {a<--<flow0 x t2}"
      using t > t2 t  existence_ivl0 x inner outer by blast
  }
  moreover {
    assume "flow0 rp dr  inner" "flow0 rp dl  outer"
    then have
      r1i: "r1  inner  {}" and
      r2o: "r2  outer  {}" using rpr1 rpr2 by auto
    from path_connected_not_frontier_subset[OF pcr1 r1i]
    have "r1  inner" using pir1 by (simp add: io(11))
    from path_connected_not_frontier_subset[OF pcr2 r2o]
    have "r2  outer" using pir2 by (simp add: io(12))

    have "(λ(x, y). flow0 x y)`({flow0 x t2} × {0<..<d})  r1" unfolding r1_def
      by (auto intro!:image_mono simp add: x2)
    then have
      *:"t. 0 < t  t < d  flow0 (flow0 x t2) t  inner"
      by (smt r1  inner greaterThanLessThan_iff mem_Sigma_iff pair_imageI r1_def subset_eq x2)

    then have t2o: "t. 0 < t  t < d  flow0 x (t2 + t)  inner"
      using r1a3[OF x2] exist flow_trans
      by (metis (no_types, opaque_lifting) closed_segment_commute ends_in_segment(1) local.existence_ivl_trans' local.flow_undefined0 real_Icc_closed_segment subset_eq t1  t2)

(* Construct a sequence of times converging to these points in r2 ⊆ outer *)
    have outer: "{a <--< flow0 x t2}  closure outer"
    proof (rule subsetI)
      fix y
      assume y: "y  {a <--< flow0 x t2}"
      have [simp]: "y  X"
        using y suba12_open suba2o {a -- b}  X
        by auto
      have "(n. flow0 y (- d / real (Suc (Suc n)))  outer)"
        using y
        using suba12_open 0 < d suba2o {a -- b}  X
        by (auto intro!: set_mp[OF r2  outer] image_eqI[where x="(y, -d/Suc (Suc n))" for n]
            simp: r2_def divide_simps) 
      moreover
      have d_over_0: "(λs. - d / real (Suc (Suc s)))  0"
        by (rule real_tendsto_divide_at_top)
          (auto intro!: filterlim_tendsto_add_at_top filterlim_real_sequentially)
      have "(λn. flow0 y (- d / real (Suc (Suc n))))  y"
        apply (rule tendsto_eq_intros)
           apply (rule tendsto_intros)
          apply (rule d_over_0)
        by auto
      ultimately show "y  closure outer"
        unfolding closure_sequential
        by (intro exI[where x="λn. flow0 y (-d/Suc (Suc n))"]) (rule conjI)
    qed
    then have "{a <--< flow0 x t1}  closure outer"
      using suba12_open by blast
    then have "{flow0 x t1 -- flow0 x t2}  closure outer"
      by (metis (no_types, lifting) closure_closure closure_mono closure_open_segment dual_order.trans outer subl x1neqx2)

    have inner:"t. t > t2  t  existence_ivl0 x  flow0 x t  inner"
    proof (rule ccontr)
      fix t
      assume t: "t > t2" "t  existence_ivl0 x" "flow0 x t  inner"
      have "0  t- (t2+d)" using t2o t by smt 
      then have a2:"0  t - (t2+dr)" using d 0 < dr dr < d by linarith
      have t2d2_ex: "t2 + dr  existence_ivl0 x"
        using t1  t2 exist d_ex[of "flow0 x t2"] flow0 x t2  {a--b} 0 < d 0 < dr dr < d 
        by (intro existence_ivl_trans) auto
      then have a3: "t - (t2 + dr)  existence_ivl0 (flow0 x (t2 + dr))"
        using t(2)
        by (intro diff_existence_ivl_trans) auto
      then have "flow0 (flow0 x (t2 + dr)) (t - (t2 + dr)) = flow0 x t"
        by (subst flow_trans[symmetric]) (auto simp: t2d2_ex)
      moreover have "flow0 x t  closure outer" using t(3) io
        by (metis ComplI Un_iff closure_Un_frontier)
      ultimately have a4: "flow0 (flow0 x (t2 + dr)) (t - (t2 + dr))  closure outer" by auto
      have a1: "flow0 x (t2+dr)  inner"
        by (simp add: d t2o 0 < dr dr < d)
      from inside_out[OF a1 a2 a3 a4]
      obtain T where T: "T > 0" "T  t - (t2 + dr)"
        "(s{0..<T}. flow0 (flow0 x (t2 + dr)) s  inner)"
        "flow0 (flow0 x (t2 + dr)) T  {flow0 x t1 --< flow0 x t2}" by blast
      define y where "y = flow0 (flow0 x (t2 + dr)) T"
      have "y  {a <--< flow0 x t2}" unfolding y_def using T(4)
        using subl2 by blast 
      then have "(λ(x, y). flow0 x y)`({y} × {-d<..<0})  r2" unfolding r2_def
        by (auto intro!:image_mono)
      then have *:"t. -d < t  t < 0  flow0 y t  r2"
        by (simp add: pair_imageI subsetD)
      have "max (-T/2) dl < 0" using d T 0 > dl dl > -d by auto
      moreover have "-d < max (-T/2) dl" using d T 0 > dl dl > -d by auto
      ultimately have outer: "flow0 y (max (-T/2) dl)  outer" using * r2  outer by blast 
      have "0(T+(max (-T/2) dl))" using T(1) by linarith
      moreover have "(T+(max (-T/2) dl)) < T" using T(1) d 0 > dl dl > -d by linarith
      ultimately have inner: " flow0 (flow0 x (t2 + dr)) (T+(max (-T/2) dl))  inner"
        using T by auto
      have T_ex: "T  existence_ivl0 (flow0 x (t2 + dr))"
        apply (subst flow_trans)
        using exist t1  t2
        using d_ex[of "flow0 x t2"] flow0 x t2  {a -- b} d > 0 T 0 < dr dr < d
          apply auto
        apply (rule set_rev_mp[where A="{0 .. t - (t2 + dr)}"], force)
        apply (rule ivl_subset_existence_ivl)
        apply (rule existence_ivl_trans')
         apply (rule existence_ivl_trans')
        by (auto simp: t)
      have T_ex2: "dr + T  existence_ivl0 (flow0 x t2)"
        by (smt T_ex ends_in_segment(2) exist local.existence_ivl_trans local.existence_ivl_trans' real_Icc_closed_segment subset_eq t2d2_ex t1  t2)
      thus False using T t1  t2 exist
        by (smt T_ex diff_existence_ivl_trans disjoint_iff_not_equal inner io(9) local.flow_trans local.flow_undefined0 outer y_def)
    qed
    have "closure outer  inner = {}"
      by (metis inf_sup_aci(1) io(2) io2(1) open_Int_closure_eq_empty)
    then have "flow0 x t  {a<--<flow0 x t2}"
      using t > t2 t  existence_ivl0 x inner outer by blast
  }
  ultimately show
    "flow0 x t  {a<--<flow0 x t2}" by auto
qed

lemma open_segment_trichotomy:
  fixes x y a b::'a
  assumes x:"x  {a<--<b}"
  assumes y:"y  {a<--<b}"
  shows "x = y  y  {x<--<b}  y  {a<--<x}"
proof -
  from Un_open_segment[OF y]
  have "{a<--<y}  {y}  {y<--<b} = {a<--<b}" .
  then have "x  {a<--<y}  x = y  x  {y <--<b}" using x by blast
  moreover {
    assume "x  {a<--<y}"
    then have "y  {x<--<b}" using open_segment_subsegment
      using open_segment_commute y by blast
  }
  moreover {
    assume "x  {y<--<b}"
    from open_segment_subsegment[OF y this]
    have "y  {a<--<x}" .
  }
  ultimately show ?thesis by blast
qed

sublocale rev: c1_on_open_R2 "-f" "-f'" rewrites "-(-f) = f" and "-(-f') = f'"
  by unfold_locales (auto simp: dim2)

lemma rev_transversal_segment: "rev.transversal_segment a b = transversal_segment a b"
  by (auto simp: transversal_segment_def rev.transversal_segment_def)

lemma flow0_transversal_segment_monotone_step_reverse:
  assumes "transversal_segment a b"
  assumes "t1  t2"
  assumes "{t1..t2}  existence_ivl0 x"
  assumes x1: "flow0 x t1  {a<--<b}"
  assumes x2: "flow0 x t2  {a<--<flow0 x t1}"
  assumes "t. t  {t1<..<t2}  flow0 x t  {a<--<b}"
  assumes "t < t1" "t  existence_ivl0 x"
  shows "flow0 x t  {a<--<flow0 x t1}"
proof -
  note exist = {t1..t2}  existence_ivl0 x
  note t1t2 = t. t  {t1<..<t2}  flow0 x t  {a<--<b}
  from transversal_segment a b have [simp]: "a  b" by (simp add: transversal_segment_def)
  from x1 obtain i1 where i1: "flow0 x t1 = line a b i1" "0 < i1" "i1 < 1"
    by (auto simp: in_open_segment_iff_line)
  from x2 obtain i2 where i2: "flow0 x t2 = line a b i2" "0 < i2" "i2 < i1"
    by (auto simp: i1 open_segment_line_iff)

  have t2_exist[simp]: "t2  existence_ivl0 x"
    using t1  t2 exist by auto
  have t2_mem: "flow0 x t2  {a<--<b}"
    and x1_mem: "flow0 x t1  {flow0 x t2<--<b}"
    using i1 i2
    by (auto simp: line_in_subsegment line_line1)

  have transversal': "rev.transversal_segment a b"
    using transversal_segment a b unfolding rev_transversal_segment .
  have time': "0  t2 - t1" using t1  t2 by simp
  have [simp, intro]: "flow0 x t2  X"
    using exist t1  t2
    by auto
  have exivl': "{0..t2 - t1}  rev.existence_ivl0 (flow0 x t2)"
    using exist t1  t2
    by (force simp add: rev_existence_ivl_eq0 intro!: existence_ivl_trans')
  have step': "rev.flow0 (flow0 x t2) (t2-t)   {a<--<rev.flow0 (flow0 x t2) (t2 - t1)}"
    apply (rule rev.flow0_transversal_segment_monotone_step[OF transversal' time' exivl'])
    using exist t1  t2 x1 x2 t2_mem x1_mem t1t2 t < t1 t  existence_ivl0 x
        apply (auto simp: rev_existence_ivl_eq0 rev_eq_flow existence_ivl_trans' flow_trans[symmetric])
    by (subst (asm) flow_trans[symmetric]) (auto intro!: existence_ivl_trans')
  then show ?thesis
    unfolding rev_eq_flow
    using t1  t2 exist t < t1 t  existence_ivl0 x
    by (auto simp: flow_trans[symmetric] existence_ivl_trans')
qed

lemma flow0_transversal_segment_monotone_step_reverse2:
  assumes transversal: "transversal_segment a b"
  assumes time: "t1  t2"
  assumes exist: "{t1..t2}  existence_ivl0 x"
  assumes t1: "flow0 x t1  {a<--<b}"
  assumes t2: "flow0 x t2  {flow0 x t1<--<b}"
  assumes t1t2: "t. t  {t1<..<t2}  flow0 x t  {a<--<b}"
  assumes t: "t < t1" "t  existence_ivl0 x"
  shows "flow0 x t  {flow0 x t1<--<b}"
  using flow0_transversal_segment_monotone_step_reverse[of b a, OF _ time exist, of t]
    assms
  by (auto simp: open_segment_commute transversal_segment_commute)

lemma flow0_transversal_segment_monotone_step2:
  assumes transversal: "transversal_segment a b"
  assumes time: "t1  t2"
  assumes exist: "{t1..t2}  existence_ivl0 x"
  assumes t1: "flow0 x t1  {a<--<b}"
  assumes t2: "flow0 x t2  {a<--<flow0 x t1}"
  assumes t1t2: "t. t  {t1<..<t2}  flow0 x t  {a<--<b}"
  shows "t. t > t2  t  existence_ivl0 x  flow0 x t  {flow0 x t2<--<b}"
  using flow0_transversal_segment_monotone_step[of b a, OF _ time exist]
    assms
  by (auto simp: transversal_segment_commute open_segment_commute)

lemma flow0_transversal_segment_monotone:
  assumes "transversal_segment a b"
  assumes "t1  t2"
  assumes "{t1..t2}  existence_ivl0 x"
  assumes x1: "flow0 x t1  {a<--<b}"
  assumes x2: "flow0 x t2  {flow0 x t1<--<b}"
  assumes "t > t2" "t  existence_ivl0 x"
  shows "flow0 x t  {a<--<flow0 x t2}"
proof -
  note exist = {t1..t2}  existence_ivl0 x
  note t = t > t2 t  existence_ivl0 x
  have x1neqx2: "flow0 x t1  flow0 x t2"
    using open_segment_def x2 by force 
  then have t1neqt2: "t1  t2" by auto
  with t1  t2 have "t1 < t2" by simp

  from transversal_segment a b have [simp]: "a  b" by (simp add: transversal_segment_def)
  from x1 obtain i1 where i1: "flow0 x t1 = line a b i1" "0 < i1" "i1 < 1"
    by (auto simp: in_open_segment_iff_line)
  from x2 i1 obtain i2 where i2: "flow0 x t2 = line a b i2" "i1 < i2" "i2 < 1"
    by (auto simp: line_open_segment_iff)
  have t2_in: "flow0 x t2  {a<--<b}"
    using i1 i2
    by simp

  let ?T = "{s  {t1..t2}. flow0 x s  {a--b}}"
  let ?T' = "{s  {t1..<t2}. flow0 x s  {a<--<b}}"
  from flow_transversal_segment_finite_intersections[OF transversal_segment a b t1  t2 exist]
  have "finite ?T" .
  then have "finite ?T'" by (rule finite_subset[rotated]) (auto simp: open_closed_segment)
  have "?T'  {}"
    by (auto intro!: exI[where x=t1] t1 < t2 x1)
  note tm_defined = finite ?T' ?T'  {}
  define tm where "tm = Max ?T'"
  have "tm  ?T'"
    unfolding tm_def
    using tm_defined by (rule Max_in)
  have tm_in: "flow0 x tm  {a<--<b}"
    using tm  ?T'
    by auto
  have tm: "t1  tm" "tm < t2" "tm  t2"
    using tm  ?T' by auto
  have tm_Max: "t  tm" if "t  ?T'" for t
    unfolding tm_def
    using tm_defined(1) that
    by (rule Max_ge)

  have tm_exclude: "flow0 x t  {a<--<b}" if "t  {tm<..<t2}" for t
    using tm  ?T' tm_Max that
    by auto (meson approximation_preproc_push_neg(2) dual_order.strict_trans2 le_cases)
  have "{tm..t2}  existence_ivl0 x"
    using exist tm by auto

  from open_segment_trichotomy[OF tm_in t2_in]
  consider
    "flow0 x t2  {flow0 x tm<--<b}" |
    "flow0 x t2  {a<--<flow0 x tm}" |
    "flow0 x tm = flow0 x t2"
    by blast
  then show "flow0 x t  {a<--<flow0 x t2}"
  proof cases
    case 1
    from flow0_transversal_segment_monotone_step[OF transversal_segment a b tm  t2
        {tm..t2}  existence_ivl0 x tm_in 1 tm_exclude t]
    show ?thesis .
  next
    case 2
    have "t1  tm"
      using 2 x2 i1 i2
      by (auto simp: line_in_subsegment line_in_subsegment2)
    then have "t1 < tm" using t1  tm by simp
    from flow0_transversal_segment_monotone_step_reverse[OF transversal_segment a b tm  t2
        {tm..t2}  existence_ivl0 x tm_in 2 tm_exclude t1 < tm] exist t1  t2
    have "flow0 x t1  {a<--<flow0 x tm}" by auto
    then have False
      using x1 x2 2 i1 i2
      apply (auto simp: line_in_subsegment line_in_subsegment2)
      by (smt greaterThanLessThan_iff in_open_segment_iff_line line_in_subsegment2 tm_in)
    then show ?thesis by simp
  next
    case 3
    have "t1  tm"
      using 3 x2
      by (auto simp: open_segment_def)
    then have "t1 < tm" using t1  tm by simp
    have "range (flow0 x) = flow0 x ` {tm..t2}"
      apply (rule recurrence_time_restricts_compact_flow'[OF tm < t2 _ _ 3])
      using exist t1  t2 t1 < tm tm < t2
      by auto
    also have " = flow0 x ` (insert t2 {tm<..<t2})"
      using tm  t2 3
      apply auto
      by (smt greaterThanLessThan_iff image_eqI)
    finally have "flow0 x t1  flow0 x ` (insert t2 {tm<..<t2})"
      by auto
    then have "flow0 x t1  flow0 x ` {tm<..<t2}" using x1neqx2
      by auto
    moreover have "  {a<--<b} = {}"
      using tm_exclude
      by auto
    ultimately have False using x1 by auto
    then show ?thesis by blast
  qed
qed

subsection ‹Straightening›

text ‹ This lemma uses the implicit function theorem ›
lemma cross_time_continuous:
  assumes "transversal_segment a b"
  assumes "x  {a<--<b}"
  assumes "e > 0"
  obtains d t where "d > 0" "continuous_on (ball x d) t"
    "y. y  ball x d  flow0 y (t y)  {a<--<b}"
    "y. y  ball x d  ¦t y¦ < e"
    "continuous_on (ball x d) t"
    "t x = 0"
proof -
  have "x  X" using assms segment_open_subset_closed[of a b]
    by (auto simp: transversal_segment_def)
  have "a  b" using assms by auto
  define s where "s x = (x - a)  rot (b - a)" for x
  have "s x = 0"
    unfolding s_def
    by (subst in_segment_inner_rot) (auto intro!: assms open_closed_segment)
  have Ds: "(s has_derivative blinfun_inner_left (rot (b - a))) (at x)"
    (is "(_ has_derivative blinfun_apply (?Ds x)) _")
    for x
    unfolding s_def
    by (auto intro!: derivative_eq_intros)
  have Dsc: "isCont ?Ds x" by (auto intro!: continuous_intros)
  have nz: "?Ds x (f x)  0"
    using assms  apply auto
    unfolding transversal_segment_def
    by (smt inner_minus_left nrm_reverse open_closed_segment)

  from flow_implicit_function_at[OF x  X, of s, OF s x = 0 Ds Dsc nz e > 0]
  obtain t d1 where "0 < d1"
    and t0: "t x = 0"
    and d1: "(y. y  cball x d1  s (flow0 y (t y)) = 0)"
    "(y. y  cball x d1  ¦t y¦ < e)"
    "(y. y  cball x d1  t y  existence_ivl0 y)"
    and tc: "continuous_on (cball x d1) t"
    and t': "(t has_derivative
        (- blinfun_inner_left (rot (b - a)) /R (blinfun_inner_left (rot (b - a))) (f x)))
      (at x)"
    by metis
  from tc
  have "t x 0"
    using 0 < d1
    by (auto simp: continuous_on_def at_within_interior t0 dest!: bspec[where x=x])
  then have ftc: "((λy. flow0 y (t y))  x) (at x)"
    by (auto intro!: tendsto_eq_intros simp: x  X)



  define e2 where "e2 = min (dist a x) (dist b x)"
  have "e2 > 0"
    using assms
    by (auto simp: e2_def open_segment_def)

  from tendstoD[OF ftc this] have "F y in at x. dist (flow0 y (t y)) x < e2" .
  moreover
  let ?S = "{x. a  (b - a) < x  (b - a)  x  (b - a) < b  (b - a)}"
  have "open ?S" "x  ?S"
    using x  {a<--<b}
    by (auto simp add: open_segment_line_hyperplanes a  b
        intro!: open_Collect_conj open_halfspace_component_gt open_halfspace_component_lt)
  from topological_tendstoD[OF ftc this] have "F y in at x. flow0 y (t y)  ?S" .
  ultimately
  have "F y in at x. flow0 y (t y)  ball x e2  ?S" by eventually_elim (auto simp: dist_commute)
  then obtain d2 where "0 < d2" and "y. x  y  dist y x < d2  flow0 y (t y)  ball x e2  ?S"
    by (force simp: eventually_at)
  then have d2: "dist y x < d2  flow0 y (t y)  ball x e2  ?S" for y
    using 0 < e2 x  X t0 x  ?S
    by (cases "y = x") auto

  define d where "d = min d1 d2"
  have "d > 0" using 0 < d1 0 < d2 by (simp add: d_def)
  moreover have "continuous_on (ball x d) t"
    by (auto intro!:continuous_on_subset[OF tc] simp add: d_def)
  moreover
  have "ball x e2  ?S  {x. s x = 0}  {a<--<b}"
    by (auto simp add: in_open_segment_iff_rot a  b) (auto simp: s_def e2_def in_segment)
  then have "y. y  ball x d  flow0 y (t y)  {a<--<b}"
    apply (rule set_mp)
    using d1 d2 0 < d2
    by (auto simp: d_def e2_def dist_commute)
  moreover have "y. y  ball x d  ¦t y¦ < e"
    using d1 by (auto simp: d_def)
  moreover have "continuous_on (ball x d) t"
    using tc by (rule continuous_on_subset) (auto simp: d_def)
  moreover have "t x = 0" by (simp add: t0)
  ultimately show ?thesis ..
qed

lemma ω_limit_crossings:
  assumes "transversal_segment a b"
  assumes pos_ex: "{0..}  existence_ivl0 x"
  assumes "ω_limit_point x p"
  assumes "p  {a<--<b}"
  obtains s where 
    "s "
    "(flow0 x  s)  p"
    "F n in sequentially. flow0 x (s n)  {a<--<b}  s n  existence_ivl0 x"
proof -
  from assms have "p  X" by (auto simp: transversal_segment_def open_closed_segment)
  from assms(3)
  obtain t where
    "t " "(flow0 x  t)  p"
    by (auto simp: ω_limit_point_def)
  note t = t  (flow0 x  t)  p
  note [tendsto_intros] = t(2)
  from cross_time_continuous[OF assms(1,4) zero_less_one― ‹TODO ??›]
  obtain τ δ
    where "0 < δ" "continuous_on (ball p δ) τ" 
      "τ p = 0" "(y. y  ball p δ  ¦τ y¦ < 1)"
      "(y. y  ball p δ  flow0 y (τ y)  {a<--<b})"
    by metis
  note τ =
    (y. y  ball p δ  flow0 y (τ y)  {a<--<b})
    (y. y  ball p δ  ¦τ y¦ < 1)
    continuous_on (ball p δ) τ τ p = 0
  define s where "s n = t n + τ (flow0 x (t n))" for n
  have ev_in_ball: "F n in at_top. flow0 x (t n)  ball p δ"
    apply simp
    apply (subst dist_commute)
    apply (rule tendstoD)
     apply (rule t[unfolded o_def])
    apply (rule 0 < δ)
    done
  have "filterlim s at_top sequentially"
  proof (rule filterlim_at_top_mono)
    show "filterlim (λn. -1 + t n) at_top sequentially"
      by (rule filterlim_tendsto_add_at_top) (auto intro!: filterlim_tendsto_add_at_top t)
    from ev_in_ball show "F x in sequentially. -1 + t x  s x"
      apply eventually_elim
      using τ
      by (force simp : s_def)
  qed
  moreover
  have τ_cont: "τ p τ p"
    using τ(3) 0 < δ
    by (auto simp: continuous_on_def at_within_ball dest!: bspec[where x=p])
  note [tendsto_intros] = tendsto_compose_at[OF _ this, simplified]
  have ev1: "F n in sequentially. t n > 1"
    using filterlim_at_top_dense t(1) by auto
  then have ev_eq: "F n in sequentially. flow0 ((flow0 x o t) n) ((τ o (flow0 x o t)) n) = (flow0 x o s) n"
    using ev_in_ball
    apply (eventually_elim)
    apply (drule τ(2))
    unfolding o_def
    apply (subst flow_trans[symmetric])
    using pos_ex
      apply (auto simp: s_def)
    apply (rule existence_ivl_trans')
    by auto
  then
  have "F n in sequentially.
  (flow0 x o s) n = flow0 ((flow0 x o t) n) ((τ o (flow0 x o t)) n)"
    by (simp add: eventually_mono)
  from (flow0 x  t)  p and τ p τ p
  have
    "(λn. flow0 ((flow0 x  t) n) ((τ  (flow0 x  t)) n))
  
  flow0 p (τ p)"
    using τ p = 0 τ_cont p  X
    by (intro tendsto_eq_intros) auto
  then have "(flow0 x o s)  flow0 p (τ p)"
    using ev_eq by (rule Lim_transform_eventually)
  then have "(flow0 x o s)  p"
    using p  X τ p = 0
    by simp
  moreover
  {
    have "F n in sequentially. flow0 x (s n)  {a<--<b}"
      using ev_eq ev_in_ball
      apply eventually_elim
      apply (drule sym)
      apply simp
      apply (rule τ) by simp
    moreover have "F n in sequentially. s n  existence_ivl0 x"
      using ev_in_ball ev1
      apply (eventually_elim)
      apply (drule τ(2))
      using pos_ex
      by (auto simp: s_def)
    ultimately have "F n in sequentially. flow0 x (s n)  {a<--<b}  s n  existence_ivl0 x"
      by eventually_elim auto
  }
  ultimately show ?thesis ..
qed

(* Obvious but frequently used step *)
lemma filterlim_at_top_tendstoE:
  assumes "e > 0"
  assumes "filterlim s at_top sequentially"
  assumes "(flow0 x  s)  u"
  assumes "F n in sequentially. P (s n)"
  obtains m where "m > b" "P m" "dist (flow0 x m) u < e"
proof -
  from assms(2) have "F n in sequentially. b < s n"
    by (simp add: filterlim_at_top_dense)
  moreover have "F n in sequentially. norm ((flow0 x  s) n - u) < e"
    using assms(3)[THEN tendstoD, OF assms(1)] by (simp add: dist_norm)
  moreover note assms(4)
  ultimately have "F n in sequentially. b < s n  norm ((flow0 x  s) n - u) < e  P (s n)"
    by eventually_elim auto
  then obtain m where "m > b" "P m" "dist (flow0 x m) u < e"
    by (auto simp add: eventually_sequentially dist_norm)
  then show ?thesis ..
qed

lemma open_segment_separate_left:
  fixes u v x a b::'a
  assumes u:"u  {a <--< b}"
  assumes v:"v  {u <--< b}"
  assumes x: "dist x u < dist u v" "x  {a <--< b}"
  shows "x  {a <--< v}"
proof -
  have "v  x"
    by (smt dist_commute x(1)) 
  moreover have "x  {v<--<b}"
    by (smt dist_commute dist_in_open_segment open_segment_subsegment v x(1))
  moreover have "v  {a<--<b}" using v
    by (metis ends_in_segment(1) segment_open_subset_closed subset_eq subset_segment(4) u)
  ultimately show ?thesis using open_segment_trichotomy[OF _ x(2)]
    by blast
qed

lemma open_segment_separate_right:
  fixes u v x a b::'a
  assumes u:"u  {a <--< b}"
  assumes v:"v  {a <--< u}"
  assumes x: "dist x u < dist u v" "x  {a <--< b}"
  shows "x  {v <--< b}"
proof -
  have "v  x"
    by (smt dist_commute x(1))
  moreover have "x  {a<--<v}"
    by (smt dist_commute dist_in_open_segment open_segment_commute open_segment_subsegment v x(1))
  moreover have "v  {a<--<b}" using v
    by (metis ends_in_segment(1) segment_open_subset_closed subset_eq subset_segment(4) u)
  ultimately show ?thesis using open_segment_trichotomy[OF _ x(2)]
    by blast
qed

lemma no_two_ω_limit_points:
  assumes transversal: "transversal_segment a b"
  assumes ex_pos: "{0..}  existence_ivl0 x"
  assumes u: "ω_limit_point x u" "u  {a<--<b}"
  assumes v: "ω_limit_point x v" "v  {a<--<b}"
  assumes uv: "v  {u<--<b}"
  shows False
proof -
  have unotv: "u  v" using uv
    using dist_in_open_segment by blast 
  define duv where "duv = dist u v / 2"
  have duv: "duv > 0" unfolding duv_def using unotv by simp
  from ω_limit_crossings[OF transversal ex_pos u]
  obtain su where su: "filterlim su at_top sequentially"
    "(flow0 x  su)  u"
    "F n in sequentially. flow0 x (su n)  {a<--<b}  su n  existence_ivl0 x" by blast
  from ω_limit_crossings[OF transversal ex_pos v]
  obtain sv where sv: "filterlim sv at_top sequentially"
    "(flow0 x  sv)  v"
    "F n in sequentially. flow0 x (sv n)  {a<--<b}  sv n  existence_ivl0 x" by blast
  from filterlim_at_top_tendstoE[OF duv su]
  obtain su1 where su1:"su1 > 0" "flow0 x su1  {a<--<b}"
    "su1  existence_ivl0 x" "dist (flow0 x su1) u < duv" by auto
  from filterlim_at_top_tendstoE[OF duv sv, of su1]
  obtain su2 where su2:"su2 > su1" "flow0 x su2  {a<--<b}"
    "su2  existence_ivl0 x" "dist (flow0 x su2) v < duv" by auto
  from filterlim_at_top_tendstoE[OF duv su, of su2]
  obtain su3 where su3:"su3 > su2" "flow0 x su3  {a<--<b}"
    "su3  existence_ivl0 x" "dist (flow0 x su3) u < duv" by auto
  have *: "su1  su2" "{su1..su2}  existence_ivl0 x" using su1 su2
     apply linarith
    by (metis atLeastatMost_empty_iff empty_iff mvar.closed_segment_subset_domain real_Icc_closed_segment su1(3) su2(3) subset_eq)

(* by construction *)
  have d1: "dist (flow0 x su1) v  (dist u v)/2" using su1(4) duv unfolding duv_def
    by (smt dist_triangle_half_r)
  have "dist (flow0 x su1) u < dist u v" using su1(4) duv unfolding duv_def by linarith
  from open_segment_separate_left[OF u(2) uv this su1(2)]
  have su1l:"flow0 x su1  {a<--<v}" .
  have "dist (flow0 x su2) v < dist v (flow0 x su1)" using d1
    by (smt dist_commute duv_def su2(4))
  from open_segment_separate_right[OF v(2) su1l this su2(2)]
  have su2l:"flow0 x su2  {flow0 x su1<--<b}" .
  then have su2ll:"flow0 x su2  {u<--<b}"
    by (smt dist_commute dist_pos_lt duv_def open_segment_subsegment pos_half_less open_segment_separate_right su2(2) su2(4) u(2) uv v(2) unotv)

  have "dist (flow0 x su2) u  (dist u v)/2" using su2(4) duv unfolding duv_def
    by (smt dist_triangle_half_r)
  then have "dist (flow0 x su3) u < dist u (flow0 x su2)"
    by (smt dist_commute duv_def su3(4)) 
  from open_segment_separate_left[OF u(2) su2ll this su3(2)]
  have su3l:"flow0 x su3  {a<--<flow0 x su2}" .

  from flow0_transversal_segment_monotone[OF transversal * su1(2) su2l su3(1) su3(3)]
  have "flow0 x su3  {a <--<flow0 x su2}" .
  thus False using su3l by auto
qed


subsection ‹Unique Intersection›

text ‹Perko Section 3.7 Remark 2›
lemma unique_transversal_segment_intersection:
  assumes "transversal_segment a b"
  assumes "{0..}  existence_ivl0 x"
  assumes "u  ω_limit_set x  {a<--<b}"
  shows "ω_limit_set x  {a<--<b} = {u}"
proof (rule ccontr)
  assume "ω_limit_set x  {a<--<b}  {u}"
  then
  obtain v where uv: "u  v"
    and v: "ω_limit_point x v" "v  {a<--<b}" using assms unfolding ω_limit_set_def
    by fastforce
  have u:"ω_limit_point x u" "u  {a<--<b}" using assms unfolding ω_limit_set_def
    by auto
  show False using no_two_ω_limit_points[OF transversal_segment a b]
    by (smt dist_commute dist_in_open_segment open_segment_trichotomy u uv v assms)
qed

text ‹Adapted from Perko Section 3.7 Lemma 4 (+ Chicone )›
lemma periodic_imp_ω_limit_set:
  assumes "compact K" "K  X"
  assumes "x  X" "trapped_forward x K"
  assumes "periodic_orbit y"
    "flow0 y ` UNIV  ω_limit_set x"
  shows "flow0 y `UNIV = ω_limit_set x"
proof (rule ccontr)
  note y = periodic_orbit y flow0 y ` UNIV  ω_limit_set x
  from trapped_sol_right[OF assms(1-4)] 
  have ex_pos: "{0..}  existence_ivl0 x" by blast
  assume "flow0 y `UNIV  ω_limit_set x"
  obtain p where p: "p  ω_limit_set x" "p  flow0 y ` UNIV"
    using y(2) apply auto
    using range (flow0 y)  ω_limit_set x by blast
  from ω_limit_set_in_compact_connected[OF assms(1-4)] have
    wcon: "connected (ω_limit_set x)" .
  from ω_limit_set_invariant have
    "invariant (ω_limit_set x)" .
  from ω_limit_set_in_compact_compact[OF assms(1-4)] have
    "compact (ω_limit_set x)" .
  then have sc: "seq_compact (ω_limit_set x)"
    using compact_imp_seq_compact by blast
  have y1:"closed (flow0 y ` UNIV)"
    using closed_orbit_ω_limit_set periodic_orbit_def ω_limit_set_closed y(1) by auto
  have y2: "flow0 y ` UNIV  {}" by simp 
  let ?py = "infdist p (range (flow0 y))"
  have "0 < ?py"
    using y1 y2 p(2)
    by (rule infdist_pos_not_in_closed)
  have "n::nat. z. z  ω_limit_set x - flow0 y ` UNIV 
    infdist z (flow0 y ` UNIV) < ?py/2^n"
  proof (rule ccontr)
    assume " ¬ (n. z. z  ω_limit_set x - range (flow0 y) 
                infdist z (range (flow0 y))
                < infdist p (range (flow0 y)) / 2 ^ n) "
    then obtain n where n: "(z  ω_limit_set x - range (flow0 y).
      infdist z (range (flow0 y))  ?py / 2 ^ n)"
      using not_less by blast
    define A where "A = flow0 y ` UNIV"
    define B where "B = {z. infdist z (range (flow0 y))  ?py / 2 ^ n}"
    have Ac:"closed A" unfolding A_def using y1 by auto
    have Bc:"closed B" unfolding B_def using infdist_closed by auto
    have "A  B = {}"
    proof (rule ccontr)
      assume "A  B  {}"
      then obtain q where q: "q  A" "q  B" by blast
      have qz:"infdist q (range(flow0 y)) = 0" using q(1) unfolding A_def
        by simp
      note 0 < ?py
      moreover have "2 ^ n > (0::real)" by auto
      ultimately have "infdist p (range (flow0 y)) / 2 ^ n > (0::real)"
        by simp
      then have qnz: "infdist q(range (flow0 y)) > 0" using q(2) unfolding B_def
        by auto
      show False using qz qnz by auto
    qed
    then have a1:"A  B  ω_limit_set x = {}" by auto
    have "ω_limit_set x - range(flow0 y)  B" using n B_def by blast
    then have a2:"ω_limit_set x  A  B" using A_def by auto
    from connected_closedD[OF wcon a1 a2 Ac Bc]
    have "A  ω_limit_set x = {}  B  ω_limit_set x = {}" .
    moreover {
      assume "A  ω_limit_set x = {}"
      then have False unfolding A_def using y(2) by blast
    }
    moreover {
      assume "B  ω_limit_set x = {}"
      then have False unfolding B_def using p
        using A_def B_def a2 by blast
    }
    ultimately show False by blast
  qed
  then obtain s where s: "n::nat. (s::nat  _) n  ω_limit_set x - flow0 y ` UNIV 
                      infdist (s n) (flow0 y ` UNIV) < ?py/2^n"
    by metis
  then have "n. s n  ω_limit_set x" by blast
  from seq_compactE[OF sc this]
  obtain l r where lr: "l  ω_limit_set x" "strict_mono r" "(s  r)  l" by blast
  have "n. infdist (s n) (range (flow0 y))  ?py / 2 ^ n" using s
    using less_eq_real_def by blast
  then have "n. norm(infdist (s n) (range (flow0 y)))  ?py / 2 ^ n"
    by (auto simp add: infdist_nonneg)
  from LIMSEQ_norm_0_pow[OF 0 < ?py _ this]
  have "((λz. infdist z (flow0 y ` UNIV))  s)  0"
    by (auto simp add:o_def)
  from LIMSEQ_subseq_LIMSEQ[OF this lr(2)]
  have "((λz. infdist z (flow0 y ` UNIV))  (s  r))  0" by (simp add: o_assoc)
  moreover have "((λz. infdist z (flow0 y ` UNIV))  (s  r))  infdist l (flow0 y ` UNIV)"
    by (auto intro!: tendsto_eq_intros tendsto_compose_at[OF lr(3)])
  ultimately have "infdist l (flow0 y `UNIV) = 0" using LIMSEQ_unique by auto
  then have lu: "l  flow0 y ` UNIV" using in_closed_iff_infdist_zero[OF y1 y2] by auto
  then have l1:"l  X"
    using closed_orbit_global_existence periodic_orbit_def y(1) by auto
      (* TODO: factor out as periodic_orbitE *)
  have l2:"f l  0"
    by (smt l  X l  range (flow0 y) closed_orbit_global_existence fixed_point_imp_closed_orbit_period_zero(2) fixpoint_sol(2) image_iff local.flows_reverse periodic_orbit_def y(1))
  from transversal_segment_exists[OF l1 l2]
  obtain a b where ab: "transversal_segment a b" "l  {a<--<b}" by blast
  then have "l  ω_limit_set x  {a<--<b}" using lr by auto
  from unique_transversal_segment_intersection[OF ab(1) ex_pos this]
  have luniq: "ω_limit_set x  {a<--<b} = {l} " .
  from cross_time_continuous[OF ab, of 1]
  obtain d t where dt: "0 < d"
    "(y. y  ball l d  flow0 y (t y)  {a<--<b})"
    "(y. y  ball l d  ¦t y¦ < 1)"
    "continuous_on (ball l d) t" "t l = 0"
    by auto
  obtain n where "(s  r) n  ball l d" using lr(3) dt(1) unfolding LIMSEQ_iff_nz
    by (metis dist_commute mem_ball order_refl)
  then have "flow0 ((s  r) n) (t ((s  r) n ))  {a<--<b}" using dt by auto
  moreover have sr: "(s  r) n  ω_limit_set x" "(s  r) n  flow0 y ` UNIV"
    using s by auto
  moreover have "flow0 ((s  r) n) (t ((s  r) n ))  ω_limit_set x"
    using invariant (ω_limit_set x) calculation unfolding invariant_def trapped_def
    by (smt ω_limit_set_in_compact_subset invariant (ω_limit_set x) assms(1-4) invariant_def order_trans range_eqI subsetD trapped_iff_on_existence_ivl0 trapped_sol)
  ultimately have "flow0 ((s  r) n) (t ((s  r) n ))  ω_limit_set x  {a<--<b}" by auto
  from unique_transversal_segment_intersection[OF ab(1) ex_pos this]
  have "flow0 ((s  r) n) (t ((s  r) n )) = l" using luniq by auto
  then have "((s  r) n) = flow0 l (-(t ((s  r) n ))) "
    by (smt UNIV_I (s  r) n  ω_limit_set x flows_reverse ω_limit_set_in_compact_existence assms(1-4)) 
  thus False using sr(2) lu
      flow0 ((s  r) n) (t ((s  r) n)) = l flow0 ((s  r) n) (t ((s  r) n))  ω_limit_set x
      closed_orbit_global_existence image_iff local.flow_trans periodic_orbit_def ω_limit_set_in_compact_existence range_eqI assms y(1)
    by smt
qed

end context c1_on_open_R2 begin

lemma α_limit_crossings:
  assumes "transversal_segment a b"
  assumes pos_ex: "{..0}  existence_ivl0 x"
  assumes "α_limit_point x p"
  assumes "p  {a<--<b}"
  obtains s where
    "s -∞"
    "(flow0 x  s)  p"
    "F n in sequentially.
    flow0 x (s n)  {a<--<b} 
    s n  existence_ivl0 x"
proof -
  from pos_ex have "{0..}  uminus ` existence_ivl0 x" by force
  from rev.ω_limit_crossings[unfolded rev_transversal_segment rev_existence_ivl_eq0 rev_eq_flow
      α_limit_point_eq_rev[symmetric], OF assms(1) this assms(3,4)]
  obtain s where "filterlim s at_top sequentially" "((λt. flow0 x (- t))  s)  p"
    "F n in sequentially. flow0 x (- s n)  {a<--<b}  s n  uminus ` existence_ivl0 x" .
  then have "filterlim (-s) at_bot sequentially"
    "(flow0 x  (-s))  p"
    "F n in sequentially. flow0 x ((-s) n)  {a<--<b}  (-s) n  existence_ivl0 x"
    by (auto simp: fun_Compl_def o_def filterlim_uminus_at_top)
  then show ?thesis ..
qed

text ‹If a positive limit point has a regular point in its positive limit set then it is periodic›
lemma ω_limit_point_ω_limit_set_regular_imp_periodic:
  assumes "compact K" "K  X"
  assumes "x  X" "trapped_forward x K"
  assumes y: "y  ω_limit_set x" "f y  0"
  assumes z: "z  ω_limit_set y  α_limit_set y" "f z  0"
  shows "periodic_orbit y  flow0 y ` UNIV = ω_limit_set x"
proof -
  from trapped_sol_right[OF assms(1-4)] have ex_pos: "{0..}  existence_ivl0 x" by blast
  from ω_limit_set_in_compact_existence[OF assms(1-4) y(1)]
  have yex: "existence_ivl0 y = UNIV" .
  from ω_limit_set_invariant
  have "invariant (ω_limit_set x)" .
  then have yinv: "flow0 y ` UNIV  ω_limit_set x" using yex unfolding invariant_def
    using trapped_iff_on_existence_ivl0 y(1) by blast 

  have zy: "ω_limit_point y z  α_limit_point y z"
    using z unfolding ω_limit_set_def α_limit_set_def by auto

  from ω_limit_set_in_compact_ω_limit_set_contained[OF assms(1-4)]
    ω_limit_set_in_compact_α_limit_set_contained[OF assms(1-4)]
  have zx:"z  ω_limit_set x" using zy y
    using z(1) by blast
  then have "z  X"
    by (metis UNIV_I local.existence_ivl_initial_time_iff ω_limit_set_in_compact_existence assms(1-4))
  from transversal_segment_exists[OF this z(2)]
  obtain a b where ab: "transversal_segment a b" "z  {a<--<b}" by blast

  from zy
  obtain t1 t2 where t1: "flow0 y t1  {a<--<b}" and t2: "flow0 y t2  {a<--<b}" and "t1  t2"
  proof
    assume zy: "ω_limit_point y z"
    from ω_limit_crossings[OF ab(1) _ zy ab(2), unfolded yex]
    obtain s where s: "filterlim s at_top sequentially"
      "(flow0 y  s)  z"
      "F n in sequentially. flow0 y (s n)  {a<--<b}"
      by auto
    from eventually_happens[OF this(3)] obtain t1 where t1: "flow0 y t1  {a<--<b}" by auto
    have "F n in sequentially. s n > t1"
      using filterlim_at_top_dense s(1) by auto
    with s(3) have "F n in sequentially. flow0 y (s n)  {a<--<b}  s n > t1"
      by eventually_elim simp
    from eventually_happens[OF this] obtain t2 where t2: "flow0 y t2  {a<--<b}" and "t1  t2"
      by auto
    from t1 this show ?thesis ..
  next
    assume zy: "α_limit_point y z"
    from α_limit_crossings[OF ab(1) _ zy ab(2), unfolded yex]
    obtain s where s: "filterlim s at_bot sequentially"
      "(flow0 y  s)  z"
      "F n in sequentially. flow0 y (s n)  {a<--<b}"
      by auto
    from eventually_happens[OF this(3)] obtain t1 where t1: "flow0 y t1  {a<--<b}" by auto
    have "F n in sequentially. s n < t1"
      using filterlim_at_bot_dense s(1) by auto
    with s(3) have "F n in sequentially. flow0 y (s n)  {a<--<b}  s n < t1"
      by eventually_elim simp
    from eventually_happens[OF this] obtain t2 where t2: "flow0 y t2  {a<--<b}" and "t1  t2"
      by auto
    from t1 this show ?thesis ..
  qed
  have "flow0 y t1  ω_limit_set x  {a<--<b}" using t1 UNIV_I yinv by auto
  moreover have "flow0 y t2  ω_limit_set x  {a<--<b}" using t2 UNIV_I yinv by auto
  ultimately have feq:"flow0 y t1 = flow0 y t2"
    using unique_transversal_segment_intersection[OF transversal_segment a b ex_pos]
    by blast
  have "t1  t2" "t1  existence_ivl0 y" "t2  existence_ivl0 y" using t1   t2
      apply blast
     apply (simp add: yex)
    by (simp add: yex)
  from periodic_orbitI[OF this feq y(2)]
  have 1: "periodic_orbit y" .
  from periodic_imp_ω_limit_set[OF assms(1-4) this yinv]
  have 2: "flow0 y` UNIV = ω_limit_set x" .
  show ?thesis using 1 2 by auto
qed

subsection ‹Poincare Bendixson Theorems›
text ‹Perko Section 3.7 Theorem 1›
theorem poincare_bendixson:
  assumes "compact K" "K  X"
  assumes "x  X" "trapped_forward x K"
  assumes "0  f ` (ω_limit_set x)"
  obtains y where "periodic_orbit y"
    "flow0 y ` UNIV = ω_limit_set x"
proof -
  note f = 0  f ` (ω_limit_set x)
  from ω_limit_set_in_compact_nonempty[OF assms(1-4)]
  obtain y where y: "y  ω_limit_set x" by fastforce
  from ω_limit_set_in_compact_existence[OF  assms(1-4) y]
  have yex: "existence_ivl0 y = UNIV" .
  from ω_limit_set_invariant
  have "invariant (ω_limit_set x)" .
  then have yinv: "flow0 y ` UNIV  ω_limit_set x" using yex unfolding invariant_def
    using trapped_iff_on_existence_ivl0 y by blast
  from ω_limit_set_in_compact_subset[OF assms(1-4)]
  have "ω_limit_set x  K" .
  then have "flow0 y ` UNIV  K" using yinv by auto
  then have yk:"trapped_forward y K"
    by (simp add: image_subsetI range_subsetD trapped_forward_def)
  have "y  X"
    by (simp add: local.mem_existence_ivl_iv_defined(2) yex)

  from ω_limit_set_in_compact_nonempty[OF assms(1-2) this _]
  obtain z where z: "z  ω_limit_set y" using yk by blast
  from ω_limit_set_in_compact_ω_limit_set_contained[OF assms(1-4)]
  have zx:"z  ω_limit_set x" using z  ω_limit_set y y by auto

  have yreg : "f y  0" using f y
    by (metis rev_image_eqI)
  have zreg : "f z  0" using f zx
    by (metis rev_image_eqI) 
  from ω_limit_point_ω_limit_set_regular_imp_periodic[OF assms(1-4) y yreg _ zreg] z
  show ?thesis using that by blast
qed

lemma fixed_point_in_ω_limit_set_imp_ω_limit_set_singleton_fixed_point:
  assumes "compact K" "K  X"
  assumes "x  X" "trapped_forward x K"
  assumes fp: "yfp  ω_limit_set x" "f yfp = 0"
  assumes zpx: "z  ω_limit_set x"
  assumes finite_fp: "finite {y  K. f y = 0}" (is "finite ?S")
  shows "(p1  ω_limit_set x. f p1 = 0  ω_limit_set z = {p1}) 
    (p2  ω_limit_set x. f p2 = 0  α_limit_set z = {p2})"
proof -
  let ?weq = "{y  ω_limit_set x. f y = 0}"
  from ω_limit_set_in_compact_subset[OF assms(1-4)]
  have wxK: "ω_limit_set x  K" .
  from ω_limit_set_in_compact_ω_limit_set_contained[OF assms(1-4)]
  have zx: "ω_limit_set z  ω_limit_set x" using zpx by auto
  have zX: "z  X" using subset_trans[OF wxK assms(2)]
    by (metis subset_iff zpx)
  from ω_limit_set_in_compact_subset[OF assms(1-4)]
  have "?weq  ?S"
    by (smt Collect_mono_iff Int_iff inf.absorb_iff1)
  then have "finite ?weq" using finite ?S
    by (blast intro: rev_finite_subset) 

  consider "f z = 0" | "f z  0" by auto
  then show ?thesis
  proof cases
    assume "f z = 0"
    from fixed_point_imp_ω_limit_set[OF zX this]
      fixed_point_imp_α_limit_set[OF zX this]
    show ?thesis
      by (metis (mono_tags) f z = 0 zpx)
  next
    assume "f z  0"
    have zweq: "ω_limit_set z  ?weq"
      apply clarsimp
    proof (rule ccontr)
      fix k assume k: "k  ω_limit_set z" "¬ (k  ω_limit_set x  f k = 0)"
      then have "f k  0" using zx k by auto
      from ω_limit_point_ω_limit_set_regular_imp_periodic[OF assms(1-4) zpx f z  0 _ this] k(1)
      have "periodic_orbit z" "range(flow0 z) = ω_limit_set x" by auto
      then have "0  f ` (ω_limit_set x)"
        by (metis image_iff periodic_orbit_imp_flow0_regular)
      thus False using fp
        by (metis (mono_tags, lifting) empty_Collect_eq image_eqI)
    qed
    have zweq0: "α_limit_set z  ?weq"
      apply clarsimp
    proof (rule ccontr)
      fix k assume k: "k  α_limit_set z" "¬ (k  ω_limit_set x  f k = 0)"
      then have "f k  0" using zx k
          ω_limit_set_in_compact_α_limit_set_contained[OF assms(1-4), of z] zpx
        by auto
      from ω_limit_point_ω_limit_set_regular_imp_periodic[OF assms(1-4) zpx f z  0 _ this] k(1)
      have "periodic_orbit z" "range(flow0 z) = ω_limit_set x" by auto
      then have "0  f ` (ω_limit_set x)"
        by (metis image_iff periodic_orbit_imp_flow0_regular)
      thus False using fp
        by (metis (mono_tags, lifting) empty_Collect_eq image_eqI)
    qed
    from ω_limit_set_in_compact_existence[OF assms(1-4) zpx]
    have zex: "existence_ivl0 z = UNIV" .
    from ω_limit_set_invariant
    have "invariant (ω_limit_set x)" .
    then have zinv: "flow0 z ` UNIV  ω_limit_set x" using zex unfolding invariant_def
      using trapped_iff_on_existence_ivl0 zpx by blast
    then have "flow0 z ` UNIV  K" using wxK by auto
    then have a2: "trapped_forward z K" "trapped_backward z K"
      using trapped_def trapped_iff_on_existence_ivl0 apply fastforce
      using range (flow0 z)  K trapped_def trapped_iff_on_existence_ivl0 by blast
    have a3: "finite (ω_limit_set z)"
      by (metis finite ?weq finite_subset zweq)
    from finite_ω_limit_set_in_compact_imp_unique_fixed_point[OF assms(1-2) zX a2(1) a3]
    obtain p1 where p1: "ω_limit_set z = {p1}" "f p1 = 0" by blast
    then have "p1  ?weq" using zweq by blast
    moreover
    have "finite (α_limit_set z)"
      by (metis finite ?weq finite_subset zweq0)
    from finite_α_limit_set_in_compact_imp_unique_fixed_point[OF assms(1-2) zX a2(2) this]
    obtain p2 where p2: "α_limit_set z = {p2}" "f p2 = 0" by blast
    then have "p2  ?weq" using zweq0 by blast
    ultimately show ?thesis
      by (simp add: p1 p2)
  qed
qed

end context c1_on_open_R2 begin

text ‹Perko Section 3.7 Theorem 2›
theorem poincare_bendixson_general:
  assumes "compact K" "K  X"
  assumes "x  X" "trapped_forward x K"
  assumes "S = {y  K. f y = 0}" "finite S"
  shows
    "(y  S. ω_limit_set x = {y}) 
  (y. periodic_orbit y 
    flow0 y ` UNIV = ω_limit_set x) 
  (P R. ω_limit_set x = P  R 
    P  S  0  f ` R  R  {} 
    (z  R.
      (p1  P. ω_limit_set z = {p1}) 
      (p2  P. α_limit_set z = {p2})))"
proof -
  note S = S = {y  K. f y = 0}
  let ?wreg = "{y  ω_limit_set x. f y  0}"
  let ?weq = "{y  ω_limit_set x. f y = 0}"
  have wreqweq: "?wreg  ?weq = ω_limit_set x"
    by (smt Collect_cong Collect_disj_eq mem_Collect_eq ω_limit_set_def)

  from trapped_sol_right[OF assms(1-4)] have ex_pos: "{0..}  existence_ivl0 x" by blast
  from ω_limit_set_in_compact_subset[OF assms(1-4)]
  have wxK: "ω_limit_set x  K" .
  then have "?weq  S" using S
    by (smt Collect_mono_iff Int_iff inf.absorb_iff1)
  then have "finite ?weq" using finite S
    by (metis rev_finite_subset) 
  from ω_limit_set_invariant
  have xinv: "invariant (ω_limit_set x)" .

  from ω_limit_set_in_compact_nonempty[OF assms(1-4)] wreqweq
  consider "?wreg = {}" |
    "?weq = {}" |
    "?weq  {}" "?wreg  {}" by auto
  then show ?thesis
  proof cases
    (* If w has no regular points then it is equal to a single unique fixed point *)
    assume "?wreg = {}"
    then have "finite (ω_limit_set x)"
      by (metis (mono_tags, lifting) {y  ω_limit_set x. f y = 0}  S finite S rev_finite_subset sup_bot.left_neutral wreqweq)
    from finite_ω_limit_set_in_compact_imp_unique_fixed_point[OF assms(1-4) this]
    obtain y where y: "ω_limit_set x = {y}" "f y = 0" by blast
    then have "y  S"
      by (metis Un_empty_left ?weq  S ?wreg = {} insert_subset wreqweq)
    then show ?thesis using y by auto
  next
    (* If w has no fixed points, then the Poincare Bendixson theorem applies *)
    assume "?weq = {}"
    then have " 0  f ` ω_limit_set x"
      by (smt empty_Collect_eq imageE)
    from poincare_bendixson[OF assms(1-4) this]
    have "(y. periodic_orbit y  flow0 y ` UNIV = ω_limit_set x)"
      by metis
    then show ?thesis by blast
  next
    (* Otherwise, all points in the limit set converge to a finite subset of the fixed points *)
    assume "?weq  {}" "?wreg  {}"
    then obtain yfp where yfp: "yfp  ω_limit_set x" "f yfp = 0" by auto
    have "0  f ` ?wreg" by auto
    have "(p1ω_limit_set x. f p1 = 0  ω_limit_set z = {p1}) 
      (p2ω_limit_set x. f p2 = 0  α_limit_set z = {p2})"
      if zpx: "z  ω_limit_set x" for z
      using fixed_point_in_ω_limit_set_imp_ω_limit_set_singleton_fixed_point[
          OF assms(1-4) yfp zpx finite S[unfolded S]] by auto
    then have "ω_limit_set x = ?weq  ?wreg 
        ?weq  S  0  f ` ?wreg  ?wreg  {} 
        (z  ?wreg.
         (p1  ?weq. ω_limit_set z = {p1}) 
         (p2  ?weq. α_limit_set z = {p2}))"
      using wreqweq ?weq  S ?wreg  {} 0  f ` ?wreg
      by blast
    then show ?thesis by blast
  qed
qed

corollary poincare_bendixson_applied:
  assumes "compact K" "K  X"
  assumes "K  {}" "positively_invariant K"
  assumes "0  f ` K"
  obtains y where "periodic_orbit y" "flow0 y ` UNIV  K"
proof -
  from assms(1-4) obtain x where "x  K" "x  X" by auto
  have *: "trapped_forward x K"
    using assms(4) x  K
    by (auto simp: positively_invariant_def)
  have subs: "ω_limit_set x  K"
    by (rule ω_limit_set_in_compact_subset[OF assms(1-2) x  X *])
  with assms(5) have "0  f ` ω_limit_set x" by auto
  from poincare_bendixson[OF assms(1-2) x  X * this]
  obtain y where "periodic_orbit y" "range (flow0 y) = ω_limit_set x"
    by force
  then have "periodic_orbit y" "flow0 y ` UNIV  K" using subs by auto
  then show ?thesis ..
qed

(*
  Limit cycles are periodic orbits that is the ω (or α)-limit set of some point not in the cycle.
  As with periodic_orbit, limit_cycles are defined for a representative point y
*)
definition "limit_cycle y 
  periodic_orbit y 
  (x. x  flow0 y ` UNIV 
  (flow0 y ` UNIV = ω_limit_set x  flow0 y ` UNIV = α_limit_set x))"

corollary poincare_bendixson_limit_cycle:
  assumes "compact K" "K  X"
  assumes "x  K" "positively_invariant K"
  assumes "0  f ` K"
  assumes "rev.flow0 x t  K"
  obtains y where "limit_cycle y" "flow0 y ` UNIV  K"
proof -
  have "x  X" using assms(2-3) by blast
  have *: "trapped_forward x K"
    using assms(3-4)
    by (auto simp: positively_invariant_def)
  have subs: "ω_limit_set x  K"
    by (rule ω_limit_set_in_compact_subset[OF assms(1-2) x  X *])
  with assms(5) have "0  f ` ω_limit_set x" by auto
  from poincare_bendixson[OF assms(1-2) x  X * this]
  obtain y where y: "periodic_orbit y" "range (flow0 y) = ω_limit_set x"
    by force
  then have c2: "flow0 y ` UNIV  K" using subs by auto
  have exy: "existence_ivl0 y = UNIV"
    using closed_orbit_global_existence periodic_orbit_def y(1) by blast
  have "x  flow0 y ` UNIV"
  proof clarsimp
    fix tt
    assume "x = flow0 y tt"
    then have "rev.flow0 (flow0 y tt) t  K" using assms(6) by auto
    moreover have "rev.flow0 (flow0 y tt) t  flow0 y ` UNIV" using exy unfolding rev_eq_flow
      using UNIV_I x = flow0 y tt closed_orbit_ω_limit_set closed_orbit_flow0 periodic_orbit_def y by auto
    ultimately show False using c2 by blast
  qed
  then have "limit_cycle y" "flow0 y ` UNIV  K" using y c2 unfolding limit_cycle_def by auto
  then show ?thesis ..
qed

end

end