Theory Poincare_Lines_Axis_Intersections

theory Poincare_Lines_Axis_Intersections
  imports Poincare_Between
begin

(* ------------------------------------------------------------------ *)
section‹Intersection of h-lines with the x-axis in the Poincar\'e model›
(* ------------------------------------------------------------------ *)

(* ---------------------------------------------------------------- *)
subsection‹Betweeness of x-axis intersection›
(* ---------------------------------------------------------------- *)

text‹The intersection point of the h-line determined by points $u$ and $v$ and the x-axis is between
$u$ and $v$, then $u$ and $v$ are in the opposite half-planes (one must be in the upper, and the
other one in the lower half-plane).›

lemma poincare_between_x_axis_intersection:
  assumes "u  unit_disc" and "v  unit_disc" and "z  unit_disc" and "u  v"
  assumes "u  circline_set x_axis" and "v  circline_set x_axis"
  assumes "z  circline_set (poincare_line u v)  circline_set x_axis"
  shows "poincare_between u z v  Arg (to_complex u) * Arg (to_complex v) < 0"
proof-
  have " u v. u  unit_disc  v  unit_disc  u  v 
       u  circline_set x_axis  v  circline_set x_axis  
       z  circline_set (poincare_line u v)  circline_set x_axis  
       (poincare_between u z v  Arg (to_complex u) * Arg (to_complex v) < 0)" (is "?P z")
  proof (rule wlog_real_zero)
    show "?P 0h"
    proof ((rule allI)+, rule impI, (erule conjE)+)
      fix u v
      assume *: "u  unit_disc" "v  unit_disc" "u  v"
                "u  circline_set x_axis" "v  circline_set x_axis"
                "0h  circline_set (poincare_line u v)  circline_set x_axis"
      obtain u' v' where uv: "u = of_complex u'" "v = of_complex v'"
        using * inf_or_of_complex[of u] inf_or_of_complex[of v]
        by auto

       
      hence "u  0h" "v  0h" "u'  0" "v'  0"
        using *
        by auto

      hence "Arg u'  0" "Arg v'  0"
        using * arg_0_iff[of u'] arg_0_iff[of v']
        unfolding circline_set_x_axis uv
        by auto

      have "poincare_collinear {0h, u, v}"
        using *
        unfolding poincare_collinear_def
        by (rule_tac x="poincare_line u v" in exI, simp)
      have "(k<0. u' = cor k * v')  (Arg u' * Arg v' < 0)" (is "?lhs  ?rhs")
      proof
        assume "?lhs"
        then obtain k where "k < 0" "u' = cor k * v'"
          by auto
        thus ?rhs
          using arg_mult_real_negative[of k v'] arg_uminus_opposite_sign[of v']
          using u'  0 v'  0 Arg u'  0 Arg v'  0
          by (auto simp add: mult_neg_pos mult_pos_neg)
      next
        assume ?rhs
        obtain ru rv φ where polar: "u' = cor ru * cis φ" "v' = cor rv * cis φ"
          using poincare_collinear {0h, u, v} poincare_collinear_zero_polar_form[of u' v'] uv * u'  0 v'  0
          by auto
        have "ru * rv < 0"
          using polar ?rhs u'  0 v'  0
          using arg_mult_real_negative[of "ru" "cis φ"] arg_mult_real_positive[of "ru" "cis φ"]
          using arg_mult_real_negative[of "rv" "cis φ"] arg_mult_real_positive[of "rv" "cis φ"]
          apply (cases "ru > 0")
          apply (cases "rv > 0", simp, simp add: mult_pos_neg)
          apply (cases "rv > 0", simp add: mult_neg_pos, simp)
          done
        thus "?lhs"
          using polar     
          by (rule_tac x="ru / rv" in exI, auto simp add: divide_less_0_iff mult_less_0_iff)
      qed
      thus "poincare_between u 0h v = (Arg (to_complex u) * Arg (to_complex v) < 0)"
        using poincare_between_u0v[of u v] * u  0h v  0h uv
        by simp
    qed
  next
    fix a z 
    assume 1: "is_real a" "cmod a < 1" "z  unit_disc"
    assume 2: "?P (moebius_pt (blaschke a) z)"
    show "?P z"
    proof ((rule allI)+, rule impI, (erule conjE)+)
      fix u v
      let ?M = "moebius_pt (blaschke a)"
      let ?Mu = "?M u"
      let ?Mv = "?M v"
      assume *: "u  unit_disc" "v  unit_disc" "u  v" "u  circline_set x_axis" "v  circline_set x_axis"
      hence "u  h" "v  h"
        by auto

      have **: " x y :: real. x * y < 0  sgn (x * y) < 0"
        by simp

      assume "z  circline_set (poincare_line u v)  circline_set x_axis"
      thus "poincare_between u z v = (Arg (to_complex u) * Arg (to_complex v) < 0)"
        using * 1 2[rule_format, of ?Mu ?Mv] cmod a < 1 is_real a blaschke_unit_disc_fix[of a]
        using inversion_noteq_unit_disc[of "of_complex a" u] u  h
        using inversion_noteq_unit_disc[of "of_complex a" v] v  h
        apply auto
        apply (subst (asm) **, subst **, subst (asm) sgn_mult, subst sgn_mult, simp)
        apply (subst (asm) **, subst (asm) **, subst (asm) sgn_mult, subst (asm) sgn_mult, simp)
        done
    qed
  next
    show "z  unit_disc" by fact
  next
    show "is_real (to_complex z)"
      using assms inf_or_of_complex[of z]
      by (auto simp add: circline_set_x_axis)
  qed
  thus ?thesis
    using assms
    by simp
qed

(* ------------------------------------------------------------------ *)
subsection‹Check if an h-line intersects the x-axis›
(* ------------------------------------------------------------------ *)

lemma x_axis_intersection_equation:
  assumes
   "H = mk_circline A B C D" and
   "(A, B, C, D)  hermitean_nonzero"
 shows "of_complex z  circline_set x_axis  circline_set H 
        A*z2 + 2*Re B*z + D = 0  is_real z" (is "?lhs  ?rhs")
proof-
  have "?lhs  A*z2 + (B + cnj B)*z + D = 0  z = cnj z"
    using assms
    using circline_equation_x_axis[of z]
    using circline_equation[of H A B C D z]
    using hermitean_elems
    by (auto simp add: power2_eq_square field_simps)
  thus ?thesis
    using eq_cnj_iff_real[of z]
    using hermitean_elems[of A B C D]
    by (simp add: complex_add_cnj complex_eq_if_Re_eq)
qed

text ‹Check if an h-line intersects x-axis within the unit disc - this could be generalized to
checking if an arbitrary circline intersects the x-axis, but we do not need that.›

definition intersects_x_axis_cmat :: "complex_mat  bool" where
  [simp]: "intersects_x_axis_cmat H = (let (A, B, C, D) = H in A = 0  (Re B)2 > (Re A)2)"

lift_definition intersects_x_axis_clmat :: "circline_mat  bool" is intersects_x_axis_cmat
  done

lift_definition intersects_x_axis :: "circline  bool" is intersects_x_axis_clmat
proof (transfer)
  fix H1 H2
  assume hh: "hermitean H1  H1  mat_zero" and "hermitean H2  H2  mat_zero"
  obtain A1 B1 C1 D1 A2 B2 C2 D2 where *: "H1 = (A1, B1, C1, D1)" "H2 = (A2, B2, C2, D2)"
    by (cases H1, cases H2, auto)
  assume "circline_eq_cmat H1 H2"
  then obtain k where k: "k  0  H2 = cor k *sm H1"
    by auto
  show "intersects_x_axis_cmat H1 = intersects_x_axis_cmat H2"
  proof-
    have "k  0  (Re A1)2 < (Re B1)2  (k * Re A1)2 < (k * Re B1)2"
      by (smt mult_strict_left_mono power2_eq_square semiring_normalization_rules(13) zero_less_power2)
    thus ?thesis
      using * k
      by auto
  qed
qed

lemma intersects_x_axis_mk_circline:
  assumes "is_real A" and "A  0  B  0"
  shows "intersects_x_axis (mk_circline A B (cnj B) A)  A = 0  (Re B)2 > (Re A)2"
proof-
  let ?H = "(A, B, (cnj B),  A)"
  have "hermitean ?H"                
    using is_real A 
    unfolding hermitean_def mat_adj_def mat_cnj_def
    using eq_cnj_iff_real 
    by auto
  moreover
  have "?H  mat_zero"
    using assms
    by auto
  ultimately
  show ?thesis
    by (transfer, transfer, auto simp add: Let_def)
qed

lemma intersects_x_axis_iff:
  assumes "is_poincare_line H"
  shows "( x  unit_disc. x  circline_set H  circline_set x_axis)  intersects_x_axis H"
proof-
  obtain Ac B C Dc where  *: "H = mk_circline Ac B C Dc" "hermitean (Ac, B, C, Dc)" "(Ac, B, C, Dc)  mat_zero"
    using ex_mk_circline[of H]
    by auto
  hence "(cmod B)2 > (cmod Ac)2" "Ac = Dc"
    using assms
    using is_poincare_line_mk_circline
    by auto

  hence "H = mk_circline (Re Ac) B (cnj B) (Re Ac)" "hermitean (cor (Re Ac),  B, (cnj B), cor (Re Ac))" "(cor (Re Ac),  B, (cnj B), cor (Re Ac))  mat_zero"
    using hermitean_elems[of Ac B C Dc] *
    by auto
  then obtain A where
    *: "H = mk_circline (cor A) B (cnj B) (cor A)" "(cor A,  B, (cnj B), cor A)  hermitean_nonzero"
    by auto

  show ?thesis
  proof (cases "A = 0")
    case True
    thus ?thesis
      using *
      using x_axis_intersection_equation[OF *(1-2), of 0]
      using intersects_x_axis_mk_circline[of "cor A" B]
      by auto
  next
    case False
    show ?thesis
    proof
      assume " x  unit_disc. x  circline_set H  circline_set x_axis"
      then obtain x where **: "of_complex x  unit_disc" "of_complex x  circline_set H  circline_set x_axis"
        by (metis inf_or_of_complex inf_notin_unit_disc)
      hence "is_real x"
        unfolding circline_set_x_axis
        using of_complex_inj
        by auto
      hence eq: "A * (Re x)2 + 2 * Re B * Re x + A = 0"
        using **
        using x_axis_intersection_equation[OF *(1-2), of "Re x"]
        by simp
      hence "(2 * Re B)2 - 4 * A * A  0"
        using discriminant_iff[of A _ "2 * Re B" A]
        using discrim_def[of A "2 * Re B" A] False
        by auto
      hence "(Re B)2  (Re A)2"
        by (simp add: power2_eq_square)
      moreover
      have "(Re B)2  (Re A)2"
      proof (rule ccontr)
        assume "¬ ?thesis"
        hence "Re B = Re A  Re B = - Re A"
          using power2_eq_iff by blast
        hence "A * (Re x)2 +  A * 2* Re x + A = 0  A * (Re x)2 - A * 2 * Re x + A = 0"
          using eq
          by auto
        hence "A * ((Re x)2 +  2* Re x + 1) = 0  A * ((Re x)2 - 2 * Re x + 1) = 0"
          by (simp add: field_simps)
        hence "(Re x)2 + 2 * Re x + 1 = 0  (Re x)2 - 2 * Re x + 1 = 0"
          using A  0
          by simp
        hence "(Re x + 1)2 = 0  (Re x - 1)2 = 0"
          by (simp add: power2_sum power2_diff field_simps)
        hence "Re x = -1  Re x = 1"
          by auto
        thus False
          using is_real x of_complex x  unit_disc
          by (auto simp add: cmod_eq_Re)
      qed
      ultimately
      show "intersects_x_axis H"
        using intersects_x_axis_mk_circline
        using *
        by auto
    next
      assume "intersects_x_axis H"
      hence "(Re B)2 > (Re A)2"
        using * False
        using intersects_x_axis_mk_circline
        by simp
      hence discr: "(2 * Re B)2 - 4 * A * A > 0"
        by (simp add: power2_eq_square)
      then obtain x1 x2 where
        eqs: "A * x12 + 2 * Re B * x1 + A = 0" "A * x22 + 2 * Re B * x2 + A = 0" "x1  x2"
        using discriminant_pos_ex[OF A  0, of "2 * Re B" A]
        using discrim_def[of A "2 * Re B" A]
        by auto
      hence "x1 * x2 = 1"
        using viette2[OF A  0, of "2 * Re B" A x1 x2] discr A  0
        by auto
      have "abs x1  1" "abs x2  1"
        using eqs discr x1 * x2 = 1
        by (auto simp add: abs_if power2_eq_square)
      hence "abs x1 < 1  abs x2 < 1"
        using x1 * x2 = 1
        by (smt mult_le_cancel_left1 mult_minus_right)
      thus "x  unit_disc. x  circline_set H  circline_set x_axis"
        using x_axis_intersection_equation[OF *(1-2), of x1]
        using x_axis_intersection_equation[OF *(1-2), of x2]
        using eqs
        by auto
    qed
  qed
qed

(* ------------------------------------------------------------------ *)
subsection‹Check if a Poincar\'e line intersects the y-axis›
(* ------------------------------------------------------------------ *)

definition intersects_y_axis_cmat :: "complex_mat  bool" where
  [simp]: "intersects_y_axis_cmat H = (let (A, B, C, D) = H in A = 0  (Im B)2 > (Re A)2)"

lift_definition intersects_y_axis_clmat :: "circline_mat  bool" is intersects_y_axis_cmat
  done

lift_definition intersects_y_axis :: "circline  bool" is intersects_y_axis_clmat
proof (transfer)
  fix H1 H2
  assume hh: "hermitean H1  H1  mat_zero" and "hermitean H2  H2  mat_zero"
  obtain A1 B1 C1 D1 A2 B2 C2 D2 where *: "H1 = (A1, B1, C1, D1)" "H2 = (A2, B2, C2, D2)"
    by (cases H1, cases H2, auto)
  assume "circline_eq_cmat H1 H2"
  then obtain k where k: "k  0  H2 = cor k *sm H1"
    by auto
  show "intersects_y_axis_cmat H1 = intersects_y_axis_cmat H2"
  proof-
    have "k  0  (Re A1)2 < (Im B1)2  (k * Re A1)2 < (k * Im B1)2"
      by (smt mult_strict_left_mono power2_eq_square semiring_normalization_rules(13) zero_less_power2)
    thus ?thesis
      using * k
      by auto
  qed
qed

lemma intersects_x_axis_intersects_y_axis [simp]:
  shows "intersects_x_axis (moebius_circline (moebius_rotation (pi/2)) H)  intersects_y_axis H"
  unfolding moebius_rotation_def moebius_similarity_def
  by simp (transfer, transfer, auto simp add: mat_adj_def mat_cnj_def)

lemma intersects_y_axis_iff:
  assumes "is_poincare_line H"
  shows "( y  unit_disc. y  circline_set H  circline_set y_axis)  intersects_y_axis H" (is "?lhs  ?rhs")
proof-
  let ?R = "moebius_rotation (pi / 2)"
  let ?H' = "moebius_circline ?R H"
  have 1: "is_poincare_line ?H'"
    using assms
    using unit_circle_fix_preserve_is_poincare_line[OF _ assms, of ?R]
    by simp

  show ?thesis
  proof
    assume "?lhs"
    then obtain y where "y  unit_disc" "y  circline_set H  circline_set y_axis"
      by auto
    hence "moebius_pt ?R y  unit_disc  moebius_pt ?R y  circline_set ?H'  circline_set x_axis"
      using rotation_pi_2_y_axis
      by (metis Int_iff circline_set_moebius_circline_E moebius_circline_comp_inv_left moebius_pt_comp_inv_left unit_disc_fix_discI unit_disc_fix_rotation)
    thus ?rhs
      using intersects_x_axis_iff[OF 1]
      using intersects_x_axis_intersects_y_axis[of H]
      by auto
  next
    assume "intersects_y_axis H"
    hence "intersects_x_axis ?H'"
      using intersects_x_axis_intersects_y_axis[of H]
      by simp
    then obtain x where *: "x  unit_disc" "x  circline_set ?H'  circline_set x_axis"
      using intersects_x_axis_iff[OF 1]
      by auto
    let ?y = "moebius_pt (-?R) x"
    have "?y  unit_disc  ?y  circline_set H  circline_set y_axis"
      using * rotation_pi_2_y_axis[symmetric]
      by (metis Int_iff circline_set_moebius_circline_E moebius_pt_comp_inv_left moebius_rotation_uminus uminus_moebius_def unit_disc_fix_discI unit_disc_fix_rotation)
    thus ?lhs
      by auto
  qed
qed

(* ------------------------------------------------------------------ *)
subsection‹Intersection point of a Poincar\'e line with the x-axis in the unit disc›
(* ------------------------------------------------------------------ *)

definition calc_x_axis_intersection_cvec :: "complex  complex  complex_vec" where
 [simp]:  "calc_x_axis_intersection_cvec A B =
    (let discr = (Re B)2 - (Re A)2 in
         (-Re(B) + sgn (Re B) * sqrt(discr), A))"

(* intersection with the x-axis for poincare lines that are euclidean circles *)
definition calc_x_axis_intersection_cmat_cvec :: "complex_mat  complex_vec" where [simp]:
  "calc_x_axis_intersection_cmat_cvec H =
    (let (A, B, C, D) = H in 
       if A  0 then
          calc_x_axis_intersection_cvec A B
       else
          (0, 1)
    )"

lift_definition calc_x_axis_intersection_clmat_hcoords :: "circline_mat  complex_homo_coords" is calc_x_axis_intersection_cmat_cvec
  by (auto split: if_split_asm)

lift_definition calc_x_axis_intersection :: "circline  complex_homo" is calc_x_axis_intersection_clmat_hcoords
proof transfer
  fix H1 H2
  assume *: "hermitean H1  H1  mat_zero" "hermitean H2  H2  mat_zero"
  obtain A1 B1 C1 D1 A2 B2 C2 D2 where hh: "H1 = (A1, B1, C1, D1)" "H2 = (A2, B2, C2, D2)"
    by (cases H1, cases H2, auto)
  assume "circline_eq_cmat H1 H2"
  then obtain k where k: "k  0" "H2 = cor k *sm H1"
    by auto

  have "calc_x_axis_intersection_cvec A1 B1 v calc_x_axis_intersection_cvec A2 B2"
    using hh k
    apply simp
    apply (rule_tac x="cor k" in exI)
    apply auto
    apply (simp add: sgn_mult power_mult_distrib)
    apply (subst right_diff_distrib[symmetric])
    apply (subst real_sqrt_mult)
    by (simp add: real_sgn_eq right_diff_distrib)

  thus "calc_x_axis_intersection_cmat_cvec H1 v
        calc_x_axis_intersection_cmat_cvec H2"
    using hh k
    by (auto simp del: calc_x_axis_intersection_cvec_def)
qed


lemma calc_x_axis_intersection_in_unit_disc:
  assumes "is_poincare_line H" "intersects_x_axis H"
  shows "calc_x_axis_intersection H  unit_disc"
proof (cases "is_line H")
  case True
  thus ?thesis
    using assms
    unfolding unit_disc_def disc_def
    by simp (transfer, transfer, auto simp add: vec_cnj_def)
next
  case False
  thus ?thesis
    using assms
    unfolding unit_disc_def disc_def
  proof (simp, transfer, transfer)
    fix H
    assume hh: "hermitean H  H  mat_zero"
    then obtain A B D where *: "H = (A, B, cnj B, D)" "is_real A" "is_real D"
      using hermitean_elems
      by (cases H) blast
    assume "is_poincare_line_cmat H"
    hence *: "H = (A, B, cnj B, A)" "is_real A"
      using *
      by auto

    assume "¬ circline_A0_cmat H"
    hence "A  0"
      using *
      by simp

    assume "intersects_x_axis_cmat H"
    hence "(Re B)2 > (Re A)2"
      using * A  0
      by (auto simp add: power2_eq_square complex.expand)

    hence "Re B  0"
      by auto

    have "Re A  0"
      using is_real A A  0
      by (auto simp add: complex.expand)

    have "sqrt((Re B)2 - (Re A)2) < sqrt((Re B)2)"
      using Re A  0
      by (subst real_sqrt_less_iff) auto
    also have "... =  sgn (Re B) * (Re B)"
      by (smt mult_minus_right nonzero_eq_divide_eq real_sgn_eq real_sqrt_abs)
    finally
    have 1: "sqrt((Re B)2 - (Re A)2) < sgn (Re B) * (Re B)"
      .

    have 2: "(Re B)2 - (Re A)2 < sgn (Re B) * (Re B) * sqrt((Re B)2 - (Re A)2)"
      using (Re B)2 > (Re A)2
      using mult_strict_right_mono[OF 1, of "sqrt ((Re B)2 - (Re A)2)"]
      by simp

    have 3: "(Re B)2 - 2*sgn (Re B)*Re B*sqrt((Re B)2 - (Re A)2) + (Re B)2 - (Re A)2 < (Re A)2"
      using mult_strict_left_mono[OF 2, of 2]
      by (simp add: field_simps)

    have "(sgn (Re B))2 = 1"
      using Re B  0
      by (simp add: sgn_if)

    hence "(-Re B + sgn (Re B) * sqrt((Re B)2 - (Re A)2))2 < (Re A)2"
      using (Re B)2 > (Re A)2 3
      by (simp add: power2_diff field_simps)

    thus "in_ocircline_cmat_cvec unit_circle_cmat (calc_x_axis_intersection_cmat_cvec H)"
      using * (Re B)2 > (Re A)2
      by (auto simp add: vec_cnj_def power2_eq_square split: if_split_asm)
  qed
qed


lemma calc_x_axis_intersection:
  assumes "is_poincare_line H" and "intersects_x_axis H"
  shows "calc_x_axis_intersection H  circline_set H  circline_set x_axis"
proof (cases "is_line H")
  case True
  thus ?thesis
    using assms
    unfolding circline_set_def
    by simp (transfer, transfer, auto simp add: vec_cnj_def)
next
  case False
  thus ?thesis
    using assms
    unfolding circline_set_def
  proof (simp, transfer, transfer)
    fix H
    assume hh: "hermitean H  H  mat_zero"
    then obtain A B D where *: "H = (A, B, cnj B, D)" "is_real A" "is_real D"
      using hermitean_elems
      by (cases H) blast
    assume "is_poincare_line_cmat H"
    hence *: "H = (A, B, cnj B, A)" "is_real A"
      using *
      by auto
    assume "¬ circline_A0_cmat H"
    hence "A  0"
      using *
      by auto

    assume "intersects_x_axis_cmat H"
    hence "(Re B)2 > (Re A)2"
      using * A  0
      by (auto simp add: power2_eq_square complex.expand)

    hence "Re B  0"
      by auto

    show "on_circline_cmat_cvec H (calc_x_axis_intersection_cmat_cvec H) 
        on_circline_cmat_cvec x_axis_cmat (calc_x_axis_intersection_cmat_cvec H)" (is "?P1  ?P2")
    proof
      show "on_circline_cmat_cvec H (calc_x_axis_intersection_cmat_cvec H)"
      proof (cases "circline_A0_cmat H")
        case True
        thus ?thesis
          using * is_poincare_line_cmat H intersects_x_axis_cmat H
          by (simp add: vec_cnj_def)
      next
        case False
        let ?x = "calc_x_axis_intersection_cvec A B"
        let ?nom = "fst ?x" and ?den = "snd ?x"
        have x: "?x = (?nom, ?den)"
          by simp

        hence "on_circline_cmat_cvec H (calc_x_axis_intersection_cvec A B)"
        proof (subst *, subst x, subst on_circline_cmat_cvec_circline_equation)
          have "(sgn(Re B))2 = 1"
            using Re B  0 sgn_pos zero_less_power2 by fastforce
          have "(sqrt((Re B)2 - (Re A)2))2 = (Re B)2 - (Re A)2"
            using (Re B)2 > (Re A)2
            by simp

          have "(-(Re B) + sgn(Re B)*sqrt((Re B)2 - (Re A)2))2 = 
                (-(Re B))2 + (sgn(Re B)*sqrt((Re B)2 - (Re A)2))2 - 2*(Re B)*sgn(Re B)*sqrt((Re B)2 - (Re A)2)"
            by (simp add: power2_diff)
          also have "... = (Re B)*(Re B) + (sgn(Re B)*sqrt((Re B)2 - (Re A)2))2 - 2*(Re B)*sgn(Re B)*sqrt((Re B)2 - (Re A)2)"
            by (simp add: power2_eq_square)
          also have "... = (Re B)*(Re B) + (sgn(Re B))2*(sqrt((Re B)2 - (Re A)2))2 - 2*(Re B)*sgn(Re B)*sqrt((Re B)2 - (Re A)2)"
            by (simp add: power_mult_distrib)
          also have "... = (Re B)*(Re B) + (Re B)2 - (Re A)2 - 2*(Re B)*sgn(Re B)*sqrt((Re B)2 - (Re A)2)"
            using (sqrt((Re B)2 - (Re A)2))2 = (Re B)2 - (Re A)2 (sgn(Re B))2 = 1
            by simp
          finally have "(-(Re B) + sgn(Re B)*sqrt((Re B)2 - (Re A)2))2 =
                        (Re B)*(Re B) + (Re B)2 - (Re A)2 - 2*(Re B)*sgn(Re B)*sqrt((Re B)2 - (Re A)2)"
            by simp           

          have "is_real ?nom" "is_real ?den"
            using is_real A
            by simp+
          hence "cnj (?nom) = ?nom" "cnj (?den) = ?den"
            by (simp add:eq_cnj_iff_real)+      
          hence "A*?nom*(cnj (?nom)) + B*?den*(cnj (?nom)) + (cnj B)*(cnj (?den))*?nom + A*?den*(cnj (?den))
                = A*?nom*?nom + B*?den*?nom + (cnj B)*?den*?nom + A*?den*?den"
            by auto
          also have "... = A*?nom*?nom + (B + (cnj B))*?den*?nom + A*?den*?den"
            by (simp add:field_simps)
          also have "... = A*?nom*?nom + 2*(Re B)*?den*?nom + A*?den*?den"
            by (simp add:complex_add_cnj)
          also have "... = A*?nom2 + 2*(Re B)*?den*?nom + A*?den*?den"
            by (simp add:power2_eq_square)
          also have "... = A*(-(Re B) + sgn(Re B)*sqrt((Re B)2 - (Re A)2))2
                           + 2*(Re B)*A*(-(Re B) + sgn(Re B)*sqrt((Re B)2 - (Re A)2)) + A*A*A"
            unfolding calc_x_axis_intersection_cvec_def
            by auto
          also have "... = A*((Re B)*(Re B) + (Re B)2 - (Re A)2 - 2*(Re B)*sgn(Re B)*sqrt((Re B)2 - (Re A)2)) 
                     + 2*(Re B)*A*(-(Re B) + sgn(Re B)*sqrt((Re B)2 - (Re A)2)) + A*A*A"
            using (-(Re B) + sgn(Re B)*sqrt((Re B)2 - (Re A)2))2 =
                        (Re B)*(Re B) + (Re B)2 - (Re A)2 - 2*(Re B)*sgn(Re B)*sqrt((Re B)2 - (Re A)2)
            by simp
          also have "... = A*((Re B)*(Re B) + (Re B)2 - A2 - 2*(Re B)*sgn(Re B)*sqrt((Re B)2 - (Re A)2)) 
                     + 2*(Re B)*A*(-(Re B) + sgn(Re B)*sqrt((Re B)2 - (Re A)2)) + A*A*A"
            using is_real A
            by simp
          also have "... = 0"
            apply (simp add:field_simps)
            by (simp add: power2_eq_square)
          finally have "A*?nom*(cnj (?nom)) + B*?den*(cnj (?nom)) + (cnj B)*(cnj (?den))*?nom + A*?den*(cnj (?den)) = 0"
            by simp       
          thus "circline_equation A B (cnj B) A ?nom ?den"
            by simp
        qed
        thus ?thesis
          using * is_poincare_line_cmat H intersects_x_axis_cmat H
          by (simp add: vec_cnj_def)
      qed
    next
      show  "on_circline_cmat_cvec x_axis_cmat (calc_x_axis_intersection_cmat_cvec H)"
        using * is_poincare_line_cmat H intersects_x_axis_cmat H is_real A
        using eq_cnj_iff_real[of A]
        by (simp add: vec_cnj_def)
    qed
  qed
qed

lemma unique_calc_x_axis_intersection:
  assumes "is_poincare_line H" and "H  x_axis"
  assumes "x  unit_disc" and "x  circline_set H  circline_set x_axis"
  shows  "x = calc_x_axis_intersection H"
proof-
  have *: "intersects_x_axis H"
    using assms
    using intersects_x_axis_iff[OF assms(1)]
    by auto
  show "x = calc_x_axis_intersection H"
    using calc_x_axis_intersection[OF assms(1) *]
    using calc_x_axis_intersection_in_unit_disc[OF assms(1) *]
    using assms
    using unique_is_poincare_line[of x "calc_x_axis_intersection H" H x_axis]
    by auto
qed

(* ------------------------------------------------------------------ *)
subsection‹Check if an h-line intersects the positive part of the x-axis›
(* ------------------------------------------------------------------ *)

definition intersects_x_axis_positive_cmat :: "complex_mat  bool" where
  [simp]: "intersects_x_axis_positive_cmat H = (let (A, B, C, D) = H in Re A  0  Re B / Re A < -1)"

lift_definition intersects_x_axis_positive_clmat :: "circline_mat  bool" is intersects_x_axis_positive_cmat
  done

lift_definition intersects_x_axis_positive :: "circline  bool" is intersects_x_axis_positive_clmat
proof (transfer)
  fix H1 H2
  assume hh: "hermitean H1  H1  mat_zero" and "hermitean H2  H2  mat_zero"
  obtain A1 B1 C1 D1 A2 B2 C2 D2 where *: "H1 = (A1, B1, C1, D1)" "H2 = (A2, B2, C2, D2)"
    by (cases H1, cases H2, auto)
  assume "circline_eq_cmat H1 H2"
  then obtain k where "k  0  H2 = cor k *sm H1"
    by auto
  thus "intersects_x_axis_positive_cmat H1 = intersects_x_axis_positive_cmat H2"
    using *
    by simp
qed

lemma intersects_x_axis_positive_mk_circline:
  assumes "is_real A" and "A  0  B  0"
  shows "intersects_x_axis_positive (mk_circline A B (cnj B) A)  Re B / Re A < -1"
proof-
  let ?H = "(A, B, (cnj B),  A)"
  have "hermitean ?H" 
    using is_real A 
    unfolding hermitean_def mat_adj_def mat_cnj_def
    using eq_cnj_iff_real 
    by auto
  moreover
  have "?H  mat_zero"
    using assms
    by auto
  ultimately
  show ?thesis
    by (transfer, transfer, auto simp add: Let_def)
qed


lemma intersects_x_axis_positive_intersects_x_axis [simp]:
  assumes "intersects_x_axis_positive H"
  shows "intersects_x_axis H"
proof-
  have " a aa.  Re a  0; Re aa / Re a < - 1; ¬ (Re a)2 < (Re aa)2   aa = 0  a = 0"
    by (smt less_divide_eq_1_pos one_less_power pos2 power2_minus power_divide zero_less_power2)
  thus ?thesis
    using assms
    apply transfer
    apply transfer
    apply (auto simp add: hermitean_def mat_adj_def mat_cnj_def)
    done
qed

lemma add_less_abs_positive_iff:
  fixes a b :: real
  assumes "abs b < abs a"
  shows "a + b > 0  a > 0"
  using assms
  by auto

lemma calc_x_axis_intersection_positive_abs':
  fixes A B :: real
  assumes "B2 > A2" and "A  0"
  shows "abs (sgn(B) * sqrt(B2 - A2) / A) < abs(-B/A)"
proof-
  from assms have "B  0"
    by auto

  have "B2 - A2 < B2"
    using A  0
    by auto
  hence "sqrt (B2 - A2) < abs B"
    using real_sqrt_less_iff[of "B2 - A2" "B2"]
    by simp
  thus ?thesis
    using assms B  0
    by (simp add: abs_mult divide_strict_right_mono)
qed

lemma calc_intersect_x_axis_positive_lemma:
  assumes "B2 > A2" and "A  0"
  shows "(-B + sgn B * sqrt(B2 - A2)) / A > 0  -B/A > 1"
proof-
  have "(-B + sgn B * sqrt(B2 - A2)) / A = -B / A + (sgn B * sqrt(B2 - A2)) / A"
    using assms
    by (simp add: field_simps)
  moreover
  have "-B / A + (sgn B * sqrt(B2 - A2)) / A > 0  - B / A > 0"
    using add_less_abs_positive_iff[OF calc_x_axis_intersection_positive_abs'[OF assms]]
    by simp
  moreover
  hence "(B/A)2 > 1"
    using assms
    by (simp add: power_divide)
  hence "B/A > 1  B/A < -1"
    by (smt one_power2 pos2 power2_minus power_0 power_strict_decreasing zero_power2)
  hence "-B / A > 0  -B / A > 1"
    by auto
  ultimately
  show ?thesis
    using assms
    by auto
qed

lemma intersects_x_axis_positive_iff':
  assumes "is_poincare_line H"
  shows "intersects_x_axis_positive H  
         calc_x_axis_intersection H  unit_disc  calc_x_axis_intersection H  circline_set H  positive_x_axis" (is "?lhs  ?rhs")
proof
  let ?x = "calc_x_axis_intersection H"
  assume ?lhs
  hence "?x  circline_set x_axis" "?x  circline_set H" "?x  unit_disc"
    using calc_x_axis_intersection_in_unit_disc[OF assms] calc_x_axis_intersection[OF assms]
    by auto
  moreover
  have "Re (to_complex ?x) > 0"
    using ?lhs assms
  proof (transfer, transfer)
    fix H
    assume hh: "hermitean H  H  mat_zero"
    obtain A B C D where *: "H = (A, B, C, D)"
      by (cases H, auto)
    assume "intersects_x_axis_positive_cmat H"
    hence **: "Re B / Re A < - 1" "Re A  0"
      using *
      by auto
    have "(Re B)2 > (Re A)2"
      using **
      by (smt divide_less_eq_1_neg divide_minus_left less_divide_eq_1_pos real_sqrt_abs real_sqrt_less_iff right_inverse_eq)
    have "is_real A" "A  0"
      using hh hermitean_elems * Re A  0 complex.expand[of A 0]
      by auto
    have "(cmod B)2 > (cmod A)2"
      using (Re B)2 > (Re A)2 is_real A
      by (smt cmod_power2 power2_less_0 zero_power2)
    have ***: "0 < (- Re B + sgn (Re B) * sqrt ((Re B)2 - (Re A)2)) / Re A"
      using calc_intersect_x_axis_positive_lemma[of "Re A" "Re B"] ** (Re B)2 > (Re A)2
      by auto

    assume "is_poincare_line_cmat H"
    hence "A = D"
      using * hh
      by simp

    have "Re ((cor (sgn (Re B)) * cor (sqrt ((Re B)2 - (Re A)2)) - cor (Re B)) / A) = (sgn (Re B) * sqrt ((Re B)2 - (Re A)2) - Re B) / Re D"
      using is_real A A = D
      by (metis (no_types, lifting) Re_complex_of_real complex_of_real_Re of_real_diff of_real_divide of_real_mult)
    thus "0 < Re (to_complex_cvec (calc_x_axis_intersection_cmat_cvec H))"
      using * hh ** *** (cmod B)2 > (cmod A)2 (Re B)2 > (Re A)2 A  0 A = D
      by simp
  qed
  ultimately
  show ?rhs
    unfolding positive_x_axis_def
    by auto
next
  let ?x = "calc_x_axis_intersection H"
  assume ?rhs
  hence "Re (to_complex ?x) > 0"  "?x  h" "?x  circline_set x_axis" "?x  unit_disc" "?x  circline_set H"
    unfolding positive_x_axis_def
    by auto
  hence "intersects_x_axis H"
    using intersects_x_axis_iff[OF assms]
    by auto
  thus ?lhs
    using Re (to_complex ?x) > 0 assms
  proof (transfer, transfer)
    fix H
    assume hh: "hermitean H  H  mat_zero"
    obtain A B C D where *: "H = (A, B, C, D)"
      by (cases H, auto)
    assume "0 < Re (to_complex_cvec (calc_x_axis_intersection_cmat_cvec H))" "intersects_x_axis_cmat H" "is_poincare_line_cmat H"
    hence **: "A  0" "0 < Re ((cor (sgn (Re B)) * cor (sqrt ((Re B)2 - (Re A)2)) - cor (Re B)) / A)"  "A = D" "is_real A" "(Re B)2 > (Re A)2"
      using * hh hermitean_elems
      by (auto split: if_split_asm)

    have "Re A  0"
      using complex.expand[of A 0] A  0 is_real A
      by auto

    have "Re ((cor (sgn (Re B)) * cor (sqrt ((Re B)2 - (Re D)2)) - cor (Re B)) / D) = (sgn (Re B) * sqrt ((Re B)2 - (Re D)2) - Re B) / Re D"
      using is_real A A = D
      by (metis (no_types, lifting) Re_complex_of_real complex_of_real_Re of_real_diff of_real_divide of_real_mult)

    thus "intersects_x_axis_positive_cmat H"
      using * ** Re A  0
      using calc_intersect_x_axis_positive_lemma[of "Re A" "Re B"]
      by simp
  qed
qed

lemma intersects_x_axis_positive_iff:
  assumes "is_poincare_line H" and "H  x_axis"
  shows "intersects_x_axis_positive H  
         ( x. x  unit_disc  x  circline_set H  positive_x_axis)" (is "?lhs  ?rhs")
proof
  assume ?lhs
  thus ?rhs
    using intersects_x_axis_positive_iff'[OF assms(1)]
    by auto
next
  assume ?rhs
  then obtain x where "x  unit_disc" "x  circline_set H  positive_x_axis"
    by auto
  thus ?lhs
    using unique_calc_x_axis_intersection[OF assms, of x]
    using intersects_x_axis_positive_iff'[OF assms(1)]
    unfolding positive_x_axis_def
    by auto
qed

(* ------------------------------------------------------------------ *)
subsection‹Check if an h-line intersects the positive part of the y-axis›
(* ------------------------------------------------------------------ *)

definition intersects_y_axis_positive_cmat :: "complex_mat  bool" where
  [simp]: "intersects_y_axis_positive_cmat H = (let (A, B, C, D) = H in Re A  0  Im B / Re A < -1)"

lift_definition intersects_y_axis_positive_clmat :: "circline_mat  bool" is intersects_y_axis_positive_cmat
  done

lift_definition intersects_y_axis_positive :: "circline  bool" is intersects_y_axis_positive_clmat
proof (transfer)
  fix H1 H2
  assume hh: "hermitean H1  H1  mat_zero" and "hermitean H2  H2  mat_zero"
  obtain A1 B1 C1 D1 A2 B2 C2 D2 where *: "H1 = (A1, B1, C1, D1)" "H2 = (A2, B2, C2, D2)"
    by (cases H1, cases H2, auto)
  assume "circline_eq_cmat H1 H2"
  then obtain k where "k  0  H2 = cor k *sm H1"
    by auto
  thus "intersects_y_axis_positive_cmat H1 = intersects_y_axis_positive_cmat H2"
    using *
    by simp
qed

lemma intersects_x_axis_positive_intersects_y_axis_positive [simp]:
  shows "intersects_x_axis_positive (moebius_circline (moebius_rotation (-pi/2)) H)  intersects_y_axis_positive H"
  using hermitean_elems
  unfolding moebius_rotation_def moebius_similarity_def
  by simp (transfer, transfer, auto simp add: mat_adj_def mat_cnj_def)

lemma intersects_y_axis_positive_iff:
  assumes "is_poincare_line H" "H  y_axis"
  shows "( y  unit_disc. y  circline_set H  positive_y_axis)  intersects_y_axis_positive H" (is "?lhs  ?rhs")
proof-
  let ?R = "moebius_rotation (-pi / 2)"
  let ?H' = "moebius_circline ?R H"
  have 1: "is_poincare_line ?H'"
    using assms
    using unit_circle_fix_preserve_is_poincare_line[OF _ assms(1), of ?R]
    by simp

  have 2: "moebius_circline ?R H  x_axis"
  proof (rule ccontr)
    assume "¬ ?thesis"
    hence "H = moebius_circline (moebius_rotation (pi/2)) x_axis"
      using moebius_circline_comp_inv_left[of ?R H]
      by auto
    thus False
      using H  y_axis
      by auto
  qed

  show ?thesis
  proof
    assume "?lhs"
    then obtain y where "y  unit_disc" "y  circline_set H  positive_y_axis"
      by auto
    hence "moebius_pt ?R y  unit_disc" "moebius_pt ?R y  circline_set ?H'  positive_x_axis"
      using rotation_minus_pi_2_positive_y_axis
      by auto
    thus ?rhs
      using intersects_x_axis_positive_iff[OF 1 2]
      using intersects_x_axis_positive_intersects_y_axis_positive[of H]
      by auto
  next
    assume "intersects_y_axis_positive H"
    hence "intersects_x_axis_positive ?H'"
      using intersects_x_axis_positive_intersects_y_axis_positive[of H]
      by simp
    then obtain x where *: "x  unit_disc" "x  circline_set ?H'  positive_x_axis"
      using intersects_x_axis_positive_iff[OF 1 2]
      by auto
    let ?y = "moebius_pt (-?R) x"
    have "?y  unit_disc  ?y  circline_set H  positive_y_axis"
      using * rotation_minus_pi_2_positive_y_axis[symmetric]
      by (metis Int_iff circline_set_moebius_circline_E image_eqI moebius_pt_comp_inv_image_left moebius_rotation_uminus uminus_moebius_def unit_disc_fix_discI unit_disc_fix_rotation)
    thus ?lhs
      by auto
  qed
qed

(* ------------------------------------------------------------------ *)
subsection‹Position of the intersection point in the unit disc›
(* ------------------------------------------------------------------ *)

text‹Check if the intersection point of one h-line with the x-axis is located more outward the edge
of the disc than the intersection point of another h-line.›

definition outward_cmat :: "complex_mat  complex_mat  bool" where
 [simp]: "outward_cmat H1 H2 = (let (A1, B1, C1, D1) = H1; (A2, B2, C2, D2) = H2
                                 in -Re B1/Re A1  -Re B2/Re A2)"
lift_definition outward_clmat :: "circline_mat  circline_mat  bool" is outward_cmat
  done
lift_definition outward :: "circline  circline  bool" is outward_clmat
  apply transfer
  apply simp
  apply (case_tac circline_mat1, case_tac circline_mat2, case_tac circline_mat3, case_tac circline_mat4)
  apply simp
  apply (erule_tac exE)+
  apply (erule_tac conjE)+
  apply simp
  done

lemma outward_mk_circline:
  assumes "is_real A1" and "is_real A2" and "A1  0  B1  0" and "A2  0  B2  0" 
  shows "outward (mk_circline A1 B1 (cnj B1) A1) (mk_circline A2 B2 (cnj B2) A2)  - Re B1 / Re A1  - Re B2 / Re A2"
proof-
  let ?H1 = "(A1, B1, (cnj B1),  A1)"
  let ?H2 = "(A2, B2, (cnj B2),  A2)"
  have "hermitean ?H1" "hermitean ?H2"
    using is_real A1 is_real A2
    unfolding hermitean_def mat_adj_def mat_cnj_def
    using eq_cnj_iff_real 
    by auto
  moreover
  have "?H1  mat_zero" "?H2  mat_zero"
    using assms
    by auto
  ultimately
  show ?thesis
    by (transfer, transfer, auto simp add: Let_def)
qed

lemma calc_x_axis_intersection_fun_mono:
  fixes x1 x2 :: real
  assumes "x1 > 1" and "x2 > x1"
  shows "x1 - sqrt(x12 - 1) > x2 - sqrt(x22 - 1)"
  using assms
proof-
  have *: "sqrt(x12 - 1) + sqrt(x22 - 1) > 0"
    using assms
    by (smt one_less_power pos2 real_sqrt_gt_zero)

  have "sqrt(x12 - 1) < x1"
    using real_sqrt_less_iff[of "x12 - 1" "x12"] x1 > 1
    by auto
  moreover
  have "sqrt(x22 - 1) < x2"
    using real_sqrt_less_iff[of "x22 - 1" "x22"] x1 > 1 x2 > x1
    by auto
  ultimately
  have "sqrt(x12 - 1) + sqrt(x22 - 1) < x1 + x2"
    by simp
  hence "(x1 + x2) / (sqrt(x12 - 1) + sqrt(x22 - 1)) > 1"
    using *
    using less_divide_eq_1_pos[of "sqrt(x12 - 1) + sqrt(x22 - 1)" "x1 + x2"]
    by simp
  hence "(x22 - x12) / (sqrt(x12 - 1) + sqrt(x22 - 1)) > x2 - x1"
    using x2 > x1
    using mult_less_cancel_left_pos[of "x2 - x1" 1 "(x2 + x1) / (sqrt(x12 - 1) + sqrt(x22 - 1))"]
    by (simp add: power2_eq_square field_simps)
  moreover
  have "(x22 - x12) = (sqrt(x12 - 1) + sqrt(x22 - 1)) * ((sqrt(x22 - 1) - sqrt(x12 - 1)))"
    using x1 > 1 x2 > x1
    by (simp add: field_simps)
  ultimately
  have "sqrt(x22 - 1) - sqrt(x12 - 1) > x2 - x1"
    using *
    by simp
  thus ?thesis
    by simp
qed

lemma calc_x_axis_intersection_mono:
  fixes a1 b1 a2 b2 :: real
  assumes "-b1/a1 > 1" and "a1  0" and "-b2/a2  -b1/a1" and "a2  0"
  shows "(-b1 + sgn b1 * sqrt(b12 - a12)) / a1  (-b2 + sgn b2 * sqrt(b22 - a22)) / a2" (is "?lhs  ?rhs")
proof-
  have "?lhs = -b1/a1 - sqrt((-b1/a1)2 - 1)"
  proof (cases "b1 > 0")
    case True
    hence "a1 < 0"
      using assms
      by (smt divide_neg_pos)
    thus ?thesis
      using b1 > 0 a1 < 0
      by (simp add: real_sqrt_divide field_simps)
  next
    case False
    hence "b1 < 0"
      using assms
      by (cases "b1 = 0") auto
    hence "a1 > 0"
      using assms
      by (smt divide_pos_neg)
    thus ?thesis
      using b1 < 0 a1 > 0
      by (simp add: real_sqrt_divide field_simps)
  qed

  moreover

  have "?rhs = -b2/a2 - sqrt((-b2/a2)2 - 1)"
  proof (cases "b2 > 0")
    case True
    hence "a2 < 0"
      using assms
      by (smt divide_neg_pos)
    thus ?thesis
      using b2 > 0 a2 < 0
      by (simp add: real_sqrt_divide field_simps)
  next
    case False
    hence "b2 < 0"
      using assms
      by (cases "b2 = 0") auto
    hence "a2 > 0"
      using assms
      by (smt divide_pos_neg)
    thus ?thesis
      using b2 < 0 a2 > 0
      by (simp add: real_sqrt_divide field_simps)
  qed

  ultimately

  show ?thesis
    using calc_x_axis_intersection_fun_mono[of "-b1/a1" "-b2/a2"]
    using assms
    by (cases "-b1/a1=-b2/a2", auto)
qed

lemma outward:
  assumes "is_poincare_line H1" and "is_poincare_line H2"
  assumes "intersects_x_axis_positive H1" and "intersects_x_axis_positive H2"
  assumes "outward H1 H2"
  shows "Re (to_complex (calc_x_axis_intersection H1))  Re (to_complex (calc_x_axis_intersection H2))"
proof-
  have "intersects_x_axis H1" "intersects_x_axis H2"
    using assms
    by auto
  thus ?thesis
    using assms
  proof (transfer, transfer)
    fix H1 H2
    assume hh: "hermitean H1  H1  mat_zero"  "hermitean H2  H2  mat_zero"
    obtain A1 B1 C1 D1 A2 B2 C2 D2 where *: "H1 = (A1, B1, C1, D1)" "H2 = (A2, B2, C2, D2)"
      by (cases H1, cases H2, auto)
    have "is_real A1" "is_real A2"
      using hermitean_elems * hh
      by auto
    assume 1: "intersects_x_axis_positive_cmat H1" "intersects_x_axis_positive_cmat H2"
    assume 2: "intersects_x_axis_cmat H1" "intersects_x_axis_cmat H2"
    assume 3: "is_poincare_line_cmat H1" "is_poincare_line_cmat H2"
    assume 4: "outward_cmat H1 H2"
    have "A1  0" "A2  0"
      using * is_real A1 is_real A2 1 complex.expand[of A1 0] complex.expand[of A2 0]
      by auto
    hence "(sgn (Re B2) * sqrt ((Re B2)2 - (Re A2)2) - Re B2) / Re A2
          (sgn (Re B1) * sqrt ((Re B1)2 - (Re A1)2) - Re B1) / Re A1"
      using calc_x_axis_intersection_mono[of "Re B1" "Re A1" "Re B2" "Re A2"]
      using 1 4 *
      by simp
    moreover
    have "(sgn (Re B2) * sqrt ((Re B2)2 - (Re A2)2) - Re B2) / Re A2 = 
          Re ((cor (sgn (Re B2)) * cor (sqrt ((Re B2)2 - (Re A2)2)) - cor (Re B2)) / A2)"
      using is_real A2 A2  0
      by (simp add: Re_divide_real)
    moreover
    have "(sgn (Re B1) * sqrt ((Re B1)2 - (Re A1)2) - Re B1) / Re A1 =
           Re ((cor (sgn (Re B1)) * cor (sqrt ((Re B1)2 - (Re A1)2)) - cor (Re B1)) / A1)"
      using is_real A1 A1  0
      by (simp add: Re_divide_real)
    ultimately
    show "Re (to_complex_cvec (calc_x_axis_intersection_cmat_cvec H2))
           Re (to_complex_cvec (calc_x_axis_intersection_cmat_cvec H1))"
      using 2 3 A1  0 A2  0 * is_real A1 is_real A2
      by (simp del: is_poincare_line_cmat_def intersects_x_axis_cmat_def)
  qed    
qed

(* ------------------------------------------------------------------ *)
subsection‹Ideal points and x-axis intersection›
(* ------------------------------------------------------------------ *)

lemma ideal_points_intersects_x_axis:               
  assumes "is_poincare_line H" and "ideal_points H = {i1, i2}" and "H  x_axis"
  shows  "intersects_x_axis H  Im (to_complex i1) * Im (to_complex i2) < 0"
  using assms
proof-
  have "i1  i2"
    using assms(1) assms(2) ex_poincare_line_points ideal_points_different(1)
    by blast

  have "calc_ideal_points H = {i1, i2}"
    using assms
    using ideal_points_unique
    by auto

  have " i1  calc_ideal_points H. 
         i2  calc_ideal_points H. 
             is_poincare_line H  H  x_axis  i1  i2  (Im (to_complex i1) * Im (to_complex i2) < 0  intersects_x_axis H)"
  proof (transfer, transfer, (rule ballI)+, rule impI, (erule conjE)+, case_tac H, case_tac i1, case_tac i2)
    fix i11 i12 i21 i22 A B C D H i1 i2
    assume H: "H = (A, B, C, D)" "hermitean H" "H  mat_zero"
    assume line: "is_poincare_line_cmat H"
    assume i1: "i1 = (i11, i12)" "i1  calc_ideal_points_cmat_cvec H"
    assume i2: "i2 = (i21, i22)" "i2  calc_ideal_points_cmat_cvec H"
    assume different: "¬ i1 v i2"
    assume not_x_axis:  "¬ circline_eq_cmat H x_axis_cmat"

    have "is_real A" "is_real D" "C = cnj B"
      using H hermitean_elems
      by auto
    have "(cmod A)2 < (cmod B)2" "A = D"
      using line H
      by auto

    let ?discr =  "sqrt ((cmod B)2 - (Re D)2)"
    let ?den = "(cmod B)2"
    let ?i1 = "B * (- D - 𝗂 * ?discr)"
    let ?i2 = "B * (- D + 𝗂 * ?discr)"

    have "i11 = ?i1  i11 = ?i2" "i12 = ?den"
         "i21 = ?i1  i21 = ?i2" "i22 = ?den"  
      using i1 i2 H line
      by (auto split: if_split_asm)
    hence i: "i11 = ?i1  i21 = ?i2  i11 = ?i2  i21 = ?i1"
      using ¬ i1 v i2 i1 i2
      by auto

    have "Im (i11 / i12) * Im (i21 / i22) = Im (?i1 / ?den) * Im (?i2 / ?den)"
      using i i12 = ?den i22 = ?den
      by auto
    also have "... = Im (?i1) * Im (?i2) / ?den2"
      by simp
    also have "... = (Im B * (Im B * (Re D * Re D)) - Re B * (Re B * ((cmod B)2 - (Re D)2))) / cmod B ^ 4"
      using (cmod B)2 > (cmod A)2 A = D
      using is_real D cmod_eq_Re[of A]
      by (auto simp add: field_simps)
    also have "... = ((Im B)2 * (Re D)2 - (Re B)2 * ((Re B)2 + (Im B)2 - (Re D)2)) / cmod B ^ 4"
    proof-
      have "cmod B * cmod B = Re B * Re B + Im B * Im B"
        by (metis cmod_power2 power2_eq_square)
      thus ?thesis
        by (simp add: power2_eq_square)
    qed
    also have "... = (((Re D)2 - (Re B)2) * ((Re B)2 + (Im B)2)) / cmod B ^ 4"
      by (simp add: power2_eq_square field_simps)
    finally have Im_product: "Im (i11 / i12) * Im (i21 / i22) = ((Re D)2 - (Re B)2) * ((Re B)2 + (Im B)2) / cmod B ^ 4"
      .

    show "Im (to_complex_cvec i1) * Im (to_complex_cvec i2) < 0  intersects_x_axis_cmat H"
    proof safe
      assume opposite: "Im (to_complex_cvec i1) * Im (to_complex_cvec i2) < 0"
      show "intersects_x_axis_cmat H"
      proof-
        have "((Re D)2 - (Re B)2) * ((Re B)2 + (Im B)2) / cmod B ^ 4 < 0"
          using Im_product opposite i1 i2
          by simp
        hence "((Re D)2 - (Re B)2) * ((Re B)2 + (Im B)2) < 0"
          by (simp add: divide_less_0_iff)
        hence "(Re D)2 < (Re B)2"
          by (simp add: mult_less_0_iff not_sum_power2_lt_zero)
        thus ?thesis
          using H A = D  is_real D
          by auto
      qed
    next
      have *: "(k. k * Im B = 1  k = 0)  Im B = 0"
        apply (safe, erule_tac x="1 / Im B" in allE)
        using divide_cancel_left by fastforce
      assume "intersects_x_axis_cmat H"
      hence "Re D = 0  (Re D)2 < (Re B)2"
        using H A = D
        by auto
      hence "(Re D)2 < (Re B)2" 
        using is_real D line  H C = cnj B
        using not_x_axis *
        by (auto simp add: complex_eq_iff)
      hence "((Re D)2 - (Re B)2) * ((Re B)2 + (Im B)2) < 0"
        by (metis add_cancel_left_left diff_less_eq mult_eq_0_iff mult_less_0_iff power2_eq_square power2_less_0 sum_squares_gt_zero_iff)
      thus "Im (to_complex_cvec i1) * Im (to_complex_cvec i2) < 0" 
        using Im_product i1 i2
        using divide_eq_0_iff divide_less_0_iff prod.simps(2) to_complex_cvec_def zero_complex.simps(1) zero_less_norm_iff 
        by fastforce
    qed
  qed
  thus ?thesis
    using assms calc_ideal_points H = {i1, i2} i1  i2
    by auto
qed

end