Impressum Morley.thy

theory Morley 


imports Complex_Axial_Symmetry 

begin

section ‹Rotations›

locale complex_rotation =
  fixes A::complex and θ::real
begin

definition ‹r z = A + (z-A)*cis(θ)›

lemma cmod_inv_rotation:‹cmod (z-A) = cmod (r z - A)›
  unfolding r_def 
  by (simp add: norm_mult)

lemma inner_ang:‹cos (∠ z1 z2)*(cmod z1 *cmod z2) = Re (innerprod z1 z2)›
proof -
  have ‹Re (innerprod z1 z2) = Re (scalprod z1 z2)›
    unfolding innerprod_def by(auto)
  then show ?thesis 
    by (metis cos_cmod_scalprod mult.commute)
qed

lemma ang_eq_cos_theta:‹z≠A ==> cos (angle_c z A (r z)) = cos (θ)›
proof -
  assume ‹z≠A›
  then have ‹innerprod (z-A) ((r z - A)) = (z-A)*cis(θ)*cnj(z - A)›  
    unfolding innerprod_def r_def by auto 
  then have f0:‹innerprod (z-A) ((r z - A)) = cmod (z-A)^2*cis(θ)›
    by (metis ab_semigroup_mult_class.mult_ac(1) complex_mult_cnj_cmod mult.commute)
  then have ‹cos (angle_c z A (r z))*cmod (z-A)*cmod(z - A) = Re (innerprod (z-A) ((r z - A)))›
    unfolding angle_c_def 
    by (metis inner_ang mult.assoc cmod_inv_rotation)
  then have ‹cos (angle_c z A (r z)) = Re (cis θ)›
    by (simp add: ‹z ≠ A› f0 power2_eq_square)
  then show ?thesis  
    by(auto simp:cis.code)
qed

lemma cdist_dist:‹cdist = dist›
  using cdist_commute dist_complex_def by fastforce

lemma ang_eq_theta:assumes h:‹z≠A› shows ‹angle_c z A (r z) = ⇂θ⇃›
proof(cases ‹angle_c z A (r z) = ⇂- θ⇃›)
  case True
  then have ‹r z = A + (z-A)*cis(-θ)›
    by (metis add_diff_cancel_left' arg_cis cdist_def cis_cmod cis_neq_zero cmod_inv_rotation 
        isoscele_iff_pr_cis_qr mult.left_commute mult.right_neutral mult_cancel_left norm_cis 
        norm_minus_commute of_real_1 r_def right_minus_eq)
  then show ?thesis 
    by (smt (verit, del_insts) True add_diff_cancel_left' angle_c_neq0 arg_cis arg_mult_eq
        canon_ang_cos canon_ang_sin cis.code cis_cnj diff_add_cancel divisors_zero r_def)
next
  case False
  have ‹cos (angle_c z A (r z)) = cos (θ)›
    using ang_eq_cos_theta h by auto
  then show ?thesis 
    by (smt (verit, ccfv_threshold) cmod_inv_rotation r_def add_diff_cancel_left' angle_c_neq0 
        angle_c_sum arg_cis canon_ang_sin cdist_def cis.code cis_neq_zero divisors_zero eq_iff_diff_eq_0 h 
        isoscele_iff_pr_cis_qr nonzero_mult_div_cancel_left nonzero_mult_div_cancel_right norm_minus_commute)
qed

lemma inj_r:‹inj r›
  unfolding inj_on_def by(auto simp:r_def)

lemma img_eqI:‹cdist A z1 = cdist A z2 ∧ angle_c z1 A z2 = θ ==> z2 = r z1›
  apply(cases ‹z1 = A ∨ z2 = A›) 
  using r_def add_minus_cancel isoscele_iff_pr_cis_qr apply force
  unfolding r_def 
  by (metis add.commute cdist_commute diff_add_cancel isoscele_iff_pr_cis_qr mult.commute)

lemma r_id_iff:‹⇂θ⇃ = 0 ⟷ r = id›
proof -
  obtain cc :: "(complex ==> complex) ==> complex" 
    and cca :: "(complex ==> complex) ==> complex" where
    f1: "∀f. (id = f ∨ f (cc f) ≠ cc f) ∧ ((∀c. f c = c) ∨ id ≠ f)"
    by (metis (no_types) eq_id_iff)
  have f2: "∀c ca ra. ca + (c - ca) * Complex (cos ra) (sin ra) = complex_rotation.r ca ra c"
    by (simp add: complex_rotation.r_def cis.code)
  then have "∀c ca. complex_rotation.r c 0 ca = ca"
    by (metis (no_types) add_diff_cancel_left' cos_zero diff_diff_eq2 
        lambda_one mult.commute one_complex.code sin_zero)
  then show ?thesis
    using f2 f1 
    by (metis (lifting, full_types) ang_eq_theta angle_c_neq0 
        canon_ang_cos canon_ang_sin complex_i_not_zero)
qed

end


lemma axial_symmetry_eq:‹axial_symmetry B C P = axial_symmetry C B P› if ‹C≠B› for C B P
  unfolding axial_symmetry_def[OF that] axial_symmetry_def[OF that[symmetric]] 
  by (metis (no_types, lifting) complex_cnj_cancel_iff eq_iff_diff_eq_0 
      minus_diff_eq nonzero_minus_divide_divide times_divide_eq_right)

lemma img_r_sym:
  assumes h:‹z1 ≠ z2› ‹z ∉ line z1 z2›
  shows ‹axial_symmetry z1 z2 z = complex_rotation.r z1 (⇂2*angle_c z z1 z2⇃) z›
proof -
  interpret complex_rotation z1 "⇂2*angle_c z z1 z2⇃" .
  let ?z = ‹axial_symmetry z1 z2 z›
  from h have ‹z1≠z› ‹z2 ≠ z›
    unfolding line_def Elementary_Complex_Geometry.collinear_def by(auto)
  then have ‹angle_c ?z z1 z2 = -angle_c z z1 z2›
    using angle_symmetry_eq h(1) h(2) by force
  then have ‹angle_c z z1 ?z = ⇂2*angle_c z z1 z2⇃›
    by (metis ‹z1 ≠ z› add.inverse_inverse angle_c_commute angle_c_commute_pi 
        angle_sum_symmetry h(1) mult_2_right mult_commute_abs)
  have ‹ cdist z1 z = cdist z1 (axial_symmetry z1 z2 z)›
    using axial_symmetry_dist1 h(1) by blast
  then show ?thesis 
    apply(intro img_eqI)
    by (metis ‹angle_c z z1 (axial_symmetry z1 z2 z) = ⇂2 * angle_c z z1 z2⇃›)
qed

lemma img_r_sym':
  assumes h:‹z1 ≠ z2› ‹z∉line z1 z2›
  shows ‹axial_symmetry z1 z2 z = complex_rotation.r z1 (⇂-2*angle_c z2 z1 z⇃) z›
  by (metis angle_c_commute angle_c_neq0 axial_symmetry_eq_line
            cancel_comm_monoid_add_class.diff_cancel complex_rotation.img_eqI
            complex_rotation.r_def h(1,2) img_r_sym mult_eq_0_iff mult_minus_left
            mult_minus_right pi_neq_zero two_pi_canonical)

lemma equality_for_pqr:
  assumes 1:‹(a2::complex)*a3≠1› and 2:‹∧z. h z = a3*z + b3› and 3:‹∧z. g z = a2*z + b2› and 4:‹g (h z) = z›
  shows ‹z = (a2*b3 + b2)/(1-a2*a3)›
proof -
  have f21:‹g (h z) = a2*a3*z + a2*b3 +b2›
    using assms by(auto simp:2 3field_simps)  
  then have ‹ g (h z) = a2*a3*z + a2*b3 +b2 ⟷ z*(1-a2*a3) = a2*b3 + b2›
    by(auto simp:field_simps 4) 
  then have ‹a2*a3 ≠1 ==> z = (a2*b3 + b2)/(1-a2*a3)›
    using f21 by(auto simp:field_simps)
  then show ?thesis using 1 by auto
qed

lemma equality_for_comp:
  assumes 2:‹∧z. h z = (a3::complex)*z + b3› and 3:‹∧z. g z = a2*z + b2›
    and 4:‹∧z. f z = a1*z +b1›
  shows ‹((f∘f∘f)∘(g∘g∘g)∘(h∘h∘h)) z = (a1*a2*a3)^3*z +(a1^2+a1+1)*b1 +a1^3*(a2^2+a2+1)*b2
 a1^3*a2^3*(a3^2+a3+1)*b3 ›
  using assms unfolding comp_def by(auto simp:fun_eq_iff power2_eq_square power3_eq_cube field_simps)

lemma eq_translation_id:
  assumes ‹h = complex_rotation.r A 0› ‹h B = B›
  shows ‹h = id›
  using assms(1) complex_rotation.r_id_iff by auto

lemma r_eqI: 
  assumes ‹A = B› ‹θ1 = θ2›
  shows ‹r A θ1 = r B θ2›
  using assms(1) assms(2) by force

lemma r_eqI': 
  assumes ‹A = B› ‹θ1 = θ2›
  shows ‹r A θ1 z = r B θ2 z›
  using assms(1) assms(2) by force

lemma composed_rotations_same_center:
  shows ‹(complex_rotation.r A θ1 ∘ complex_rotation.r A θ2) = complex_rotation.r A (θ1 + θ2)›
  unfolding complex_rotation.r_def by (auto simp: fun_eq_iff cis_mult add_ac)


lemma composed_rotations:
  assumes h:‹⇂θ1 + θ2⇃ ≠ 0›
  shows ‹(complex_rotation.r A θ1 ∘ complex_rotation.r B θ2) =
 complex_rotation.r ((A*(1-cis θ1) + B*cis θ1*(1-cis θ2))/(1-cis (θ1+θ2))) (θ1 + θ2)›
proof -
  have ‹cis (θ1 + θ2) ≠ 1›
    by (metis arg_cis assms cis_zero zero_canonical)
  with h have ‹(complex_rotation.r A θ1 ∘ complex_rotation.r B θ2)
 ((A*(1-cis θ1) + B*cis θ1*(1-cis θ2))/(1-cis (θ1+θ2)))
 = (A*(1-cis θ1) + B*cis θ1*(1-cis θ2))/(1-cis (θ1+θ2)) ›
    unfolding complex_rotation.r_def using assms 
    by(auto simp:cis_mult field_simps  intro!:) 
  with h show ?thesis
    apply(cases ‹θ1 = 0 ∨ θ2 = 0›)
    unfolding complex_rotation.r_def using assms 
    by(auto simp:cis_mult field_simps fun_eq_iff diff_divide_distrib add_divide_distrib intro!:) 
qed


lemma composed_rotation_is_trans:
  assumes ‹⇂θ1 + θ2⇃ = 0›  
  shows ‹(complex_rotation.r A θ1 ∘ complex_rotation.r B θ2) z = z + (B - A)*(cis(θ1) - 1)›
  using assms  
  by (auto simp:complex_rotation.r_def add_divide_distrib diff_divide_distrib field_simps) 
    (metis add.commute canon_ang_cos canon_ang_sin cis.code cis_mult cis_zero lambda_one mult.commute)

section ‹Morley's theorem›

text ‹We begin by proving the Morley's theorem in the case where angles are positives
  using the congruence between two triangles with the same angles only not of the same sign
  prove Morley's theorem when angles are negatives.

  then proceed to conclude because in a triangle either angles are all negatives or all the
  are positives depending on orientation.›

theorem Morley_pos:
  assumes‹¬collinear A B C›
    ‹angle_c A B R = angle_c A B C / 3› (is ‹?abr = ?abc›)
    "angle_c B A R = angle_c B A C / 3" (is ‹?bar = ?α›)
    "angle_c B C P = angle_c B C A / 3" (is ‹?bcp = ?bca›)
    "angle_c C B P = angle_c C B A / 3" (is ‹?cbp = ?β›)
    "angle_c C A Q = angle_c C A B / 3" (is ‹?caq = ?cab›)
    "angle_c A C Q = angle_c A C B / 3" (is ‹?acq = ?γ›)
    and hhh:‹⇂angle_c B A C / 3+angle_c C B A / 3+angle_c A C B / 3⇃ = pi/3›
  shows  ‹cdist R P = cdist P Q ∧ cdist Q R = cdist P Q›
proof -
  have bundle_line:‹A∉ line B C› ‹B∉ line A C› ‹C ∉ line A B› ‹A≠B› ‹B≠C› ‹C≠A›
    using assms(1) non_collinear_independant by (auto simp:collinear_sym1 collinear_sym2 line_def) 
  {fix A B C γ
    assume ABC_nline:‹A ∉ line B C›
      and eq_3c:‹angle_c A C B = 3*γ›
    then have neq_PI:‹abs γ < pi/3›
    proof - 
      have ‹angle_c A C B ≠ pi›
        using ABC_nline(1) unfolding line_def  
        by (metis angle_c_commute_pi collinear_iff mem_Collect_eq non_collinear_independant)
      then have ‹angle_c A C B ∈ {-pi<..<pi}›
        using ang_c_in less_eq_real_def by auto
      then show ‹abs γ < pi/3›
        using eq_3c by force
    qed}note ang_inf_pi3=this
  have ‹⇂angle_c B A C + angle_c C B A + angle_c A C B⇃ = pi›
    by (metis collinear_def add.commute 
        angle_sum_triangle_c assms(1) collinear_sym1 collinear_sym2')
  have eq_pi:‹⇂3*?α + 3*?β + 3*?γ⇃ = pi›
    using ‹⇂angle_c B A C + angle_c C B A + angle_c A C B⇃ = pi› by force
  then have neq_pi:‹⇂?β⇃ ≠ pi ∧ ⇂?γ⇃ ≠ pi ∧ ⇂?α⇃ ≠ pi›
    by (smt (verit) ang_neg_neg angle_c_commute angle_c_neq0 assms 
        canon_ang_sin collinear_angle collinear_sin_neq_0 divide_eq_0_iff divide_nonneg_pos 
        minus_divide_left pi_neq_zero sin_pi sin_pi_minus zero_canonical)
  moreover have ‹3*?α ≠ 0∧3*?β ≠ 0∧3*?γ ≠ 0›
    using bundle_line collinear_sin_neq_0 line_def angle_c_commute assms(1) bundle_line(4) 
      bundle_line(5) bundle_line(6) collinear_iff assms(1) collinear_sin_neq_0 
    by (metis collinear_sym2' divide_eq_eq_numeral1(1) mem_Collect_eq mult.commute zero_neq_numeral)
  ultimately have neq_0:‹⇂?β⇃ ≠ 0 ∧ ⇂?γ⇃ ≠ 0 ∧ ⇂?α⇃ ≠ 0›
    by (metis ang_vec_def angle_c_def arg_cis assms(3) assms(5) assms(7) canon_ang_arg mult_zero_right)

  interpret rot1: complex_rotation A "2*?α" .
  interpret rot2: complex_rotation B "2*?β" .
  interpret rot3: complex_rotation C "2*?γ" .

  let ?f=‹rot1.r›
  have f0:‹rot1.r A = A›
    unfolding rot1.r_def by auto
  have f1:‹rot2.r B = B›
    unfolding rot2.r_def by auto
  have f2:‹rot3.r C = C›
    unfolding rot3.r_def by auto

  have ‹cmod (rot3.r z - C) = cmod (z-C)› for z
    using rot3.cmod_inv_rotation by presburger
  have f2:‹B≠C›
    by (metis collinear_def assms(1) collinear_sym1 collinear_sym2)
  have f5:‹angle_c C B P = ?β› ‹angle_c P B C = -?β›
    by (auto simp add: assms(5) angle_c_commute) 
      (metis angle_c_commute angle_c_commute_pi assms(5) neq_pi pi_canonical)
  then have f3:‹P ∉ line C B›
    by (smt (verit, ccfv_SIG) neq_0 neq_pi angle_c_commute angle_c_neq0 assms(4)
        collinear_angle divide_eq_0_iff line_def mem_Collect_eq pi_canonical zero_canonical)
  then have f3':‹P ∉ line B C›
    using collinear_sym2' line_def by blast
  then have f4:‹P≠C ∧ P≠B›
    by (metis collinear_def collinear_sym1 collinear_sym2 line_def mem_Collect_eq)
  then have ‹angle_c P B C = - angle_c (axial_symmetry B C P) B C›
    using angle_symmetry_eq[OF f2 _ _ f3'] by auto
  then have ‹angle_c (axial_symmetry B C P) B C = ?β›
    using f5(2) by fastforce

  have f13:‹angle_c P C B = ?γ›
    by (smt (verit, ccfv_threshold) angle_c_commute angle_c_commute_pi assms(1) assms(4) assms(7) 
        collinear_sin_neq_0 nonzero_minus_divide_divide nonzero_minus_divide_right sin_pi)
  let ?P'= ‹(axial_symmetry B C P)›

  have ‹angle_c (axial_symmetry B C P) B P = ⇂2*?β⇃›
    by (metis ‹P ≠ C ∧ P ≠ B› ‹angle_c (axial_symmetry B C P) B C = angle_c C B A / 3›
        angle_sum_symmetry f2 f5(1) involution_symmetry mult.commute mult_2_right z1_inv)
  have ‹cdist B (P) = cdist B ?P'›
    by(auto)(metis cmod_axial_inv f2 z1_inv)
  then have ‹cdist B (rot2.r P) = cdist B ?P'›
    unfolding cdist_def 
    using rot2.cmod_inv_rotation by presburger
  have f16:‹rot2.r ?P' = P›
    by (metis ‹angle_c (axial_symmetry B C P) B P = ⇂2 * (angle_c C B A / 3)⇃›
        ‹cdist B P = cdist B (axial_symmetry B C P)› canon_ang_cos
        canon_ang_sin cis.code complex_rotation.img_eqI complex_rotation.r_def)
  have f10:‹angle_c P C B = ⇂?γ⇃›
    by (metis ‹angle_c P C B = angle_c A C B / 3› ang_vec_def angle_c_def arg_cis canon_ang_arg)

  from f10 have f11:‹angle_c B C ?P' = ⇂?γ⇃›
    by (metis axial_symmetry_eq ‹P ≠ C ∧ P ≠ B› ‹angle_c P C B = angle_c A C B / 3› angle_c_commute 
        angle_symmetry angle_symmetry_eq_imp axial_symmetry_eq_line canon_ang_uminus_pi f2 f3 pi_canonical)
  then have f12:‹angle_c P C ?P' = ⇂2*?γ⇃›
    by (metis axial_symmetry_eq f13 angle_sum_symmetry f10 f2 f4 mult.commute mult_2_right)
  then have f15:‹rot3.r P = ?P'›
    by (metis axial_symmetry_eq canon_ang_cos canon_ang_sin cis.code f13 f2 f3 img_r_sym complex_rotation.r_def)
  have P_inv:‹rot2.r (rot3.r P) = P›
    using f16 f15 by presburger
  let ?Q'=‹axial_symmetry A C Q›
  have ‹angle_c C A Q = -?α›
    by (metis angle_c_commute assms(1) assms(6) collinear_sin_neq_0
        collinear_sym1 collinear_sym2' minus_divide_left sin_pi)
  then have ‹angle_c Q A C = ?α›
    by (metis add.inverse_inverse angle_c_commute canon_ang_uminus_pi neq_pi pi_canonical)
  have ‹A≠C ∧ Q∉line A C›
    by (metis ‹angle_c Q A C = angle_c B A C / 3› angle_c_neq0 assms(7) collinear_angle div_0 
        f10 f13 line_def mem_Collect_eq neq_0 neq_pi zero_canonical)
  then have f17:‹rot1.r Q = ?Q'›
    using img_r_sym[of A C Q] 
    using ‹angle_c Q A C = angle_c B A C / 3› canon_ang_cos canon_ang_sin cis.code complex_rotation.r_def 
    by presburger
  then have ‹angle_c ?Q' C A = ?γ›
    by (smt (verit, ccfv_SIG) ‹A ≠ C ∧ Q ∉ line A C› ‹angle_c Q A C = angle_c B A C / 3›
        complex_rotation.ang_eq_theta angle_c_commute angle_symmetry angle_symmetry_eq_imp assms(7) 
        axial_symmetry_eq axial_symmetry_eq_line f10 f13 complex_rotation.img_eqI neq_0 neq_pi)
  then have ‹angle_c A C Q = ?γ›
    using assms(7) by blast
  then have ‹angle_c ?Q' C Q =⇂2*?γ⇃›
    by (metis ‹A ≠ C ∧ Q ∉ line A C› ‹angle_c (axial_symmetry A C Q) C A = angle_c A C B / 3›
        ‹angle_c Q A C = angle_c B A C / 3› angle_c_neq0 angle_sum_symmetry angle_symmetry_eq
        axial_symmetry_eq involution_symmetry mult_2_right mult_commute_abs neg_equal_0_iff_equal
        neq_0 zero_canonical)
  then have f18:‹rot3.r ?Q' = Q›
    using  img_r_sym[of C A ?Q']
    by (metis ‹A ≠ C ∧ Q ∉ line A C› axial_symmetry_dist1 
        axial_symmetry_eq canon_ang_cos canon_ang_sin cis.code 
        complex_rotation.img_eqI complex_rotation.r_def)
  have Q_inv:‹rot3.r (rot1.r Q) = Q›
    using f17 f18 by presburger
  let ?R'=‹axial_symmetry A B R›
  have ‹angle_c B A R = ?α›
    by (simp add: assms(3))
  then have ‹angle_c R A B = -?α›
    by (metis angle_c_commute canon_ang_uminus_pi neq_pi pi_canonical)
  have ‹angle_c R B A = ?β›
    by (metis ‹angle_c (axial_symmetry B C P) B C = angle_c C B A / 3› angle_c_commute 
        angle_c_commute_pi assms(1) assms(2) collinear_sin_neq_0 collinear_sym1 minus_divide_left sin_pi)
  have ‹A≠B ∧ R∉line A B›
    by (metis (no_types, opaque_lifting) ‹angle_c Q A C = angle_c B A C / 3› ‹angle_c R A B = -
 angle_c B A C / 3)› angle_c_commute angle_c_commute_pi angle_c_neq0 assms(2) collinear_angle 
        collinear_sym2' diff_zero divide_eq_0_iff line_def mem_Collect_eq minus_diff_eq neg_equal_zero 
        neq_0 zero_canonical)
  then have f17:‹rot2.r R = ?R'›
    using img_r_sym[of B A R] 
    using ‹angle_c R B A = angle_c C B A / 3› axial_symmetry_eq 
      cis.code collinear_sym2 line_def complex_rotation.r_def by auto
  then have ‹angle_c ?R' A B = ?α›
    by (metis ‹A ≠ B ∧ R ∉ line A B› ‹angle_c R A B = - (angle_c B A C / 3)›
        ‹angle_c R B A = angle_c C B A / 3› add.inverse_inverse add.inverse_neutral angle_c_neq0 
        angle_symmetry_eq neq_0 zero_canonical)
  then have f18:‹rot1.r ?R' = R›
    using img_r_sym[of A B ?R'] 
    by (metis ‹A ≠ B ∧ R ∉ line A B› axial_symmetry_eq canon_ang_cos canon_ang_sin cis.code
        involution_symmetry line_is_inv complex_rotation.r_def z2_inv)
  have R_inv:‹rot1.r (rot2.r R) = R›
    using f17 f18 by presburger
  let ?a1 = ‹cis(2*?α)› let ?b1=‹A*(1-?a1)› let ?a2=‹cis(2*?β)› let ?b2=‹B*(1-?a2)›
  let ?a3=‹cis(2*?γ)› let ?b3=‹C*(1-?a3)›
  have possi_abc:‹⇂?α+?β+?γ⇃ =pi/3 ∨ ⇂?α+?β+?γ⇃ = -pi/3 ∨ ⇂?α+?β+?γ⇃ = pi›
  proof -
    have ‹⇂?α+?β+?γ⇃∈{-pi<..pi}›
      by (simp add: canon_ang(1) canon_ang(2))
    then have ‹3*⇂?α+?β+?γ⇃ ∈ {-3*pi<..3*pi}›
      by(auto) 
    then have ‹⇂⇂?α+?β+?γ⇃+⇂?α+?β+?γ⇃+⇂?α+?β+?γ⇃⇃ = ⇂?α+?β+?γ+?α+?β+?γ+?α+?β+?γ⇃›
      by (smt (verit, ccfv_SIG) add.commute arg_cis canon_ang_arg 
          canon_ang_sum distrib_left is_num_normalize(1) mult_2)
    then have ‹⇂3*⇂?α+?β+?γ⇃⇃=pi›
      using eq_pi by argo
    then have ‹3*⇂?α+?β+?γ⇃ = 3*pi ∨ 3*⇂?α+?β+?γ⇃ = -pi ∨ 3*⇂?α+?β+?γ⇃=pi›
      by (smt (verit, del_insts) canon_ang(1) canon_ang(2) canon_ang_id
          canon_ang_minus_3pi_minus_pi canon_ang_pi_3pi)
    then show ?thesis 
      by force
  qed
  have jj:‹B ∉ line C A› ‹Q ∉ line A C› ‹R ∉ line A B›
    using assms f3' ‹A ≠ C ∧ Q ∉ line A C› ‹A ≠ B ∧ R ∉ line A B›  
    by (simp_all add: collinear_sym1 collinear_sym2 line_def)
  then have inf_pi3:‹abs ?α < pi/3› ‹abs ?β < pi/3› ‹abs ?γ < pi/3›
    using ang_inf_pi3[of B C A ?α] ang_inf_pi3[of C A B ?β] ang_inf_pi3[of A B C ?γ] 
    by (auto simp add:collinear_sym2 collinear_sym1 assms line_def) 
  then have ‹abs (?α+?β+?γ) < pi›
    by argo
  have j1:‹⇂?α+?β+?γ⇃ = pi/3 ==> ?a1*?a2*?a3 = root3›
  proof -
    assume hh:‹⇂?α+?β+?γ⇃ = pi/3›
    have f20:‹cis (2 * (angle_c B A C / 3)) * cis (2 * (angle_c C B A / 3)) * cis (2 * (angle_c A C B / 3))
 = cis (2*(?α+?β+?γ))›
      by (simp add: cis_mult)
    then have f21:‹cis (2*(⇂?α+?β+?γ⇃)) = cis (2*(?α+?β+?γ))›
      by (smt (verit, ccfv_threshold) canon_ang_cos canon_ang_sin canon_ang_sum cis.code)  
    with hh show ?thesis 
      by (metis (no_types, opaque_lifting) f21  f20 times_divide_eq_right root3_def)
  qed
  have ‹rot1.r∘rot1.r = complex_rotation.r A (4*?α)›
    using composed_rotations_same_center  by auto
  have g10:‹((rot1.r∘rot1.r∘rot1.r)∘(rot2.r∘rot2.r∘rot2.r)∘(rot3.r ∘rot3.r∘rot3.r)) =
 complex_rotation.r A (6*?α) ∘ complex_rotation.r B (6*?β) ∘ complex_rotation.r C (6*?γ)›
    using composed_rotations_same_center by auto
  have f26:‹⇂6*?α + 6*?β + 6*?γ⇃ = 0›
    by (smt (verit, ccfv_SIG) canon_ang_sum eq_pi two_pi_canonical)
  also have ‹⇂6*?γ⇃ ≠ 0›
  proof (rule ccontr)
    assume ‹¬ ⇂6 * (angle_c A C B / 3)⇃ ≠ 0›
    then obtain k::int where  ‹6 * ⇂(angle_c A C B / 3)⇃ = 2*k*pi›
      by (metis add.commute add.inverse_neutral add_0 canon_ang(3) 
          diff_conv_add_uminus f10 f13 of_int_mult of_int_numeral)
    then have ‹3*⇂(angle_c A C B / 3)⇃ = k*pi›
      by force
    then show False 
      by (metis (no_types, opaque_lifting) assms(1) collinear_sin_neq_0 divide_eq_eq_numeral1(1)
          f10 f13 mult_1 sin_kpi times_divide_eq_left zero_neq_numeral)
  qed
  then have f24:‹⇂6*?α + 6*?β⇃ ≠ 0›
    by (metis add.commute add.right_neutral arg_cis calculation
        canon_ang_cos canon_ang_sin canon_ang_sum cis.code)
  let ?A1=‹(A*(1-cis (6*?α)) + B*cis (6*?α)*(1-cis (6*?β)))/(1-cis (6*?β+6*?α))›
  have g11:‹complex_rotation.r A (6*?α) ∘ complex_rotation.r B (6*?β) ∘ complex_rotation.r C (6*?γ) =
 complex_rotation.r ?A1 (6*?α + 6*?β)∘ complex_rotation.r C (6*?γ) ›
    using composed_rotations[of ‹6*?α› ‹6*?β› A B, OF f24]  
    by argo
  then have f27:‹complex_rotation.r ?A1 (6*?α + 6*?β)∘ complex_rotation.r C (6*?γ) = (λz. z + (C -
 (A * (1 - cis (6 * (angle_c B A C / 3))) + B * cis (6 * (angle_c B A C / 3)) * (1 - cis (6 * (angle_c C B A / 3)))) /
 (1 - cis (6 * (angle_c C B A / 3) + 6 * (angle_c B A C / 3)))) *
 (cis (6 * (angle_c B A C / 3) + 6 * (angle_c C B A / 3)) - 1))› (is ‹?l = (λz. z + ?A2)›)
    using composed_rotation_is_trans[of ‹6*?α + 6*?β› ‹6*?γ› ?A1 C, OF f26] 
    by auto
  have f30:‹2*angle_c A C B = 6*?γ›
    by auto
  have ‹axial_symmetry C B A = complex_rotation.r C (⇂2*angle_c A C B⇃) A›
    using img_r_sym collinear_sym1 f2 jj(1) line_def by auto
  then have first:‹complex_rotation.r C (6*?γ) A = axial_symmetry C B A› (is ‹?rr = ?axA›)
    using canon_ang_cos canon_ang_sin cis.code f30 complex_rotation.r_def by presburger
  have f31:‹axial_symmetry B C ?axA = complex_rotation.r B (⇂2*angle_c ?axA B C⇃) ?axA›
    by (metis ‹A ≠ C ∧ Q ∉ line A C› ‹⇂6 * (angle_c A C B / 3)⇃ ≠ 0›
        ‹complex_rotation.r C (6 * (angle_c A C B / 3)) A = axial_symmetry C B A›
        complex_rotation.ang_eq_theta angle_c_neq0 
        axial_symmetry_eq f2 img_r_sym involution_symmetry line_is_inv z1_inv)
  have f32:‹angle_c C B A = 3*?β›
    by simp
  then have f33:‹angle_c ?axA B C = 3*?β›
    by (smt (verit) ‹A ≠ B ∧ R ∉ line A B› ‹A ≠ C ∧ Q ∉ line A C› ‹⇂6 * (angle_c A C B / 3)⇃ ≠ 0›
        ‹complex_rotation.r C (6 * (angle_c A C B / 3)) A = axial_symmetry C B A›
        complex_rotation.ang_eq_theta angle_c_commute angle_c_neq0 angle_symmetry_eq assms(1) 
        axial_symmetry_eq collinear_sin_neq_0 collinear_sym1 f2 line_is_inv sin_pi)
  then have snd:‹complex_rotation.r B (6*?β) ((axial_symmetry B C A)) = A›
    by (smt (verit, ccfv_SIG) ‹A ≠ C ∧ Q ∉ line A C› ‹⇂6 * (angle_c A C B / 3)⇃ ≠ 0›
        ‹complex_rotation.r C (6 * (angle_c A C B / 3)) A = axial_symmetry C B A›
        complex_rotation.ang_eq_theta angle_c_neq0 axial_symmetry_eq canon_ang_cos canon_ang_sin
        cis.code f2 img_r_sym involution_symmetry line_is_inv complex_rotation.r_def z1_inv)
  then have thrd:‹complex_rotation.r A (6*?α) A = A›
    unfolding complex_rotation.r_def by auto
  then have ‹(complex_rotation.r A (6*?α) ∘ complex_rotation.r B (6*?β) ∘ complex_rotation.r C (6*?γ)) A = A›
    apply(simp) 
    by (smt (verit, best) axial_symmetry_eq f30 f32 first snd)
  then have g21:‹((rot1.r∘rot1.r∘rot1.r)∘(rot2.r∘rot2.r∘rot2.r)∘(rot3.r ∘rot3.r∘rot3.r)) = (λz. z + ?A2)›
    apply(subst g10) apply(subst g11) apply(subst f27) by(simp add:fun_eq_iff) 
  then have ‹?A2 = 0›
    by (metis ‹(complex_rotation.r A (6 * (angle_c B A C / 3)) ∘
 complex_rotation.r B (6 * (angle_c C B A / 3)) ∘
 complex_rotation.r C (6 * (angle_c A C B / 3))) A = A›
        add_diff_cancel_left' cancel_comm_monoid_add_class.diff_cancel g10)
  then have g22:‹((rot1.r∘rot1.r∘rot1.r)∘(rot2.r∘rot2.r∘rot2.r)∘(rot3.r ∘rot3.r∘rot3.r)) = id›
    using g21 by(auto simp:fun_eq_iff)
  have g20:‹rot1.r z = ?a1*z +?b1› ‹rot2.r z =?a2*z + ?b2› ‹rot3.r z = ?a3 * z + ?b3› for z
    by(auto simp:field_simps complex_rotation.r_def) 
  then  have ‹((rot1.r∘rot1.r∘rot1.r)∘(rot2.r∘rot2.r∘rot2.r)∘(rot3.r ∘rot3.r∘rot3.r)) z = (cis (2 * (angle_c B A C / 3)) * cis (2 * (angle_c C B A / 3))
 * cis (2 * (angle_c A C B / 3))) ^ 3 * z +
 ((cis (2 * (angle_c B A C / 3)))² + cis (2 * (angle_c B A C / 3)) + 1) * (A * (1 - cis (2 * (angle_c B A C / 3)))) +
 cis (2 * (angle_c B A C / 3)) ^ 3 * ((cis (2 * (angle_c C B A / 3)))² + cis (2 * (angle_c C B A / 3)) + 1) *
 (B * (1 - cis (2 * (angle_c C B A / 3)))) +
 cis (2 * (angle_c B A C / 3)) ^ 3 * cis (2 * (angle_c C B A / 3)) ^ 3 *
 ((cis (2 * (angle_c A C B / 3)))² + cis (2 * (angle_c A C B / 3)) + 1) *
 (C * (1 - cis (2 * (angle_c A C B / 3))))› (is ‹?l z = ?A3 z›) for z 
    using equality_for_comp[of rot3.r ?a3 ?b3 rot2.r ?a2 ?b2 rot1.r ?a1 ?b1, OF g20(3) g20(2) g20(1)] 
    by blast
  then have ‹z = ?A3 z› for z 
    by (metis g22 id_apply)
  then have very_imp:‹((cis (2 * (angle_c B A C / 3)))² + cis (2 * (angle_c B A C / 3)) + 1) * (A * (1 - cis (2 * (angle_c B A C / 3)))) +
 cis (2 * (angle_c B A C / 3)) ^ 3 * ((cis (2 * (angle_c C B A / 3)))² + cis (2 * (angle_c C B A / 3)) + 1) *
 (B * (1 - cis (2 * (angle_c C B A / 3)))) +
 cis (2 * (angle_c B A C / 3)) ^ 3 * cis (2 * (angle_c C B A / 3)) ^ 3 *
 ((cis (2 * (angle_c A C B / 3)))² + cis (2 * (angle_c A C B / 3)) + 1) *
 (C * (1 - cis (2 * (angle_c A C B / 3)))) = 0›
    by (metis comm_monoid_add_class.add_0 mult_zero_class.mult_zero_right)
  {assume hhh:‹⇂?α+?β+?γ⇃ = pi/3›
    have j5:‹?a1*?a2 ≠1›
    proof(rule ccontr)
      assume ‹¬ cis (2 * (angle_c B A C / 3)) * cis (2 * (angle_c C B A / 3)) ≠ 1›
      then have ‹?a1*?a2 = cis 0›
        using cis_zero by presburger
      then have ‹⇂2*(?α+?β)⇃ = 0›
        by (metis arg_cis cis_mult distrib_left zero_canonical)
      then have t:‹⇂?α+?β⇃ = pi ∨ ⇂?α+?β⇃ = 0›
        by (smt (verit, del_insts) canon_ang(1) canon_ang_id canon_ang_sum canon_ang_uminus)
      then have ‹⇂?α+?β⇃ = 0 ==> False›
        by (metis add_0 assms(1) canon_ang_sum collinear_sin_neq_0 
            divide_cancel_right f10 f13 hhh sin_pi zero_neq_numeral)
      then have ‹⇂1/3*(3*?α+3*?β)⇃=pi› using t by(auto simp:algebra_simps)
      then have ‹⇂(pi-⇂3*?γ⇃)⇃ = ⇂(3*?α+3*?β)⇃›
        by (smt (verit, ccfv_SIG) canon_ang_diff eq_pi)
      then have ‹⇂(pi/3-⇂?γ⇃)⇃ = pi›
        by (smt (verit, best) ‹⇂angle_c B A C / 3 + angle_c C B A / 3⇃ = 0 ==> False›
            canon_ang_diff hhh t)
      then have ‹⇂?γ⇃ ∈ {0<..<pi/3}›
        by (smt (verit, ccfv_SIG) add_divide_distrib ang_vec_bounded angle_c_def 
            arccos_minus_one_half arccos_one_half arcsin_minus_one_half arcsin_one_half 
            arcsin_plus_arccos canon_ang_id canon_ang_pi_3pi divide_cancel_right f13 field_sum_of_halves)
      then show False 
        using ‹⇂pi / 3 - ⇂angle_c A C B / 3⇃⇃ = pi› add_divide_distrib canon_ang_id by auto
    qed
    have r_eq_all:‹rot1.r z = ?a1*z + ?b1› ‹rot2.r z = ?a2*z + ?b2› ‹rot3.r z = ?a3*z+?b3› for z
      by(auto simp:field_simps complex_rotation.r_def cis.code) 
    have f21:‹rot2.r (rot3.r P) = ?a2*?a3*P + ?a2*?b3 +?b2›
      apply(subst r_eq_all(2)) apply(subst r_eq_all(3)) by(auto simp:field_simps) 

    then have ‹ rot2.r (rot3.r P) = ?a2*?a3*P + ?a2*?b3 +?b2 ⟷ P*(1-?a2*?a3) = ?a2*?b3 + ?b2›
      by (smt (verit) add.commute add_diff_cancel_left' add_diff_eq f15 
f16 mult.commute mult.right_neutral right_diff_distrib')
    then have j2:‹?a2*?a3 ≠1 ==> P = (?a2*?b3 + ?b2)/(1-?a2*?a3)›
      using f21 by(auto simp:field_simps) 
    have j4:‹?a1*?a3 ≠ 1›
    proof(rule ccontr)
      assume ‹¬ cis (2 * (angle_c B A C / 3)) * cis (2 * (angle_c A C B / 3)) ≠ 1›
      then have ‹?a1*?a3 = cis 0›
        using cis_zero by presburger
      then have ‹⇂2*(?α+?γ)⇃ = 0›
        by (metis arg_cis cis_mult distrib_left zero_canonical)
      then have t:‹⇂?α+?γ⇃ = pi ∨ ⇂?α+?γ⇃ = 0›
        by (smt (verit, del_insts) canon_ang(1) canon_ang_id canon_ang_sum canon_ang_uminus)
      then have k0:‹⇂?α+?γ⇃ = 0 ==> False›
        by (smt (verit, ccfv_SIG) ‹A ≠ B ∧ R ∉ line A B› ‹A ≠ C ∧ Q ∉ line A C›
            ‹∣angle_c B A C / 3 + angle_c C B A / 3 + angle_c A C B / 3∣ < pi›
            ‹angle_c (axial_symmetry A B R) A B = angle_c B A C / 3› ‹angle_c R A B = - (angle_c B A C / 3)›
            ‹angle_c R B A = angle_c C B A / 3› ang_pos_pos assms(3) canon_ang_id f2 f30 f32 neq_0 z1_inv)

      then have ‹⇂1/3*(3*?α+3*?γ)⇃=pi› using t by(auto simp:algebra_simps)
      then have ‹⇂(pi-⇂3*?β⇃)⇃ = ⇂(3*?α+3*?γ)⇃›
        by (smt (verit, ccfv_SIG) canon_ang_diff eq_pi)
      then have ‹⇂(pi/3-⇂?β⇃)⇃ = pi›
        by (smt (verit, best) k0
            canon_ang_diff hhh t)
      then have k1:‹⇂?β⇃ ∈ {0<..<pi/3}›
        by (smt (verit, del_insts) arccos_one_half arcsin_one_half arcsin_plus_arccos
            canon_ang_id divide_nonneg_pos field_sum_of_halves inf_pi3(2) pi_ge_zero)
      then show False 
        using k1 add_divide_distrib canon_ang_id ‹⇂pi / 3 - ⇂angle_c C B A / 3⇃⇃ = pi› by auto
    qed
    have j3:‹?a2*?a3 ≠ 1›
    proof(rule ccontr)
      assume ‹¬ cis (2 * (angle_c C B A / 3)) * cis (2 * (angle_c A C B / 3)) ≠ 1›
      then have ‹?a2*?a3 = cis 0›
        using cis_zero by presburger
      then have ‹⇂2*(?β+?γ)⇃ = 0›
        by (metis arg_cis cis_mult distrib_left zero_canonical)
      then have t:‹⇂?β+?γ⇃ = pi ∨ ⇂?β+?γ⇃ = 0›
        by (smt (verit, del_insts) canon_ang(1) canon_ang_id canon_ang_sum canon_ang_uminus)
      then have k0:‹⇂?β+?γ⇃ = 0 ==> False›
        by (smt (verit, ccfv_SIG) ‹A ≠ B ∧ R ∉ line A B› ‹A ≠ C ∧ Q ∉ line A C›
            ‹∣angle_c B A C / 3 + angle_c C B A / 3 + angle_c A C B / 3∣ < pi›
            ‹angle_c (axial_symmetry A B R) A B = angle_c B A C / 3› ‹angle_c R A B = - (angle_c B A C / 3)›
            ‹angle_c R B A = angle_c C B A / 3› ang_pos_pos assms(3) canon_ang_id f2 f30 f32 neq_0 z1_inv)

      then have ‹⇂1/3*(3*?β+3*?γ)⇃=pi› using t by(auto simp:algebra_simps)
      then have ‹⇂(pi-⇂3*?α⇃)⇃ = ⇂(3*?β+3*?γ)⇃›
        by (smt (verit, ccfv_SIG) canon_ang_diff eq_pi)
      then have ‹⇂(pi/3-⇂?α⇃)⇃ = pi›
        by (smt (verit, best) k0
            canon_ang_diff hhh t)
      then have k1:‹⇂?α⇃ ∈ {0<..<pi/3}›
        by (smt (verit, del_insts) arccos_one_half arcsin_one_half arcsin_plus_arccos
            canon_ang_id divide_nonneg_pos field_sum_of_halves inf_pi3(1) pi_ge_zero)
      then show False 
        using k1 add_divide_distrib canon_ang_id ‹⇂(pi/3-⇂?α⇃)⇃ = pi› by auto
    qed
    have f21':‹rot3.r (rot1.r Q) = ?a3*?a1*Q + ?a3*?b1 +?b3›
      apply(subst r_eq_all(1)) apply(subst r_eq_all(3)) by(auto simp:field_simps) 
    have f21'':‹rot1.r (rot2.r R) = ?a1*?a2*R + ?a1*?b2 +?b1›
      apply(subst r_eq_all(1)) apply(subst r_eq_all(2)) by(auto simp:field_simps) 
    have jjj:‹?a1 ≠ 0 ∧ ?a2 ≠ 0 ∧ ?a3 ≠ 0›
      using cis_neq_zero by blast
    then have eq_j:‹?a1*?a2*?a3 = root3›
      using j1 hhh by blast
    then have P_def:‹P = (?a2*?b3 + ?b2)/(1-?a2*?a3)›(is ‹_=?P›)
      using j2 j3 by blast
    have n1: ‹1-?a2*?a3 = (?a1 - root3)/?a1›
      by (smt (verit, ccfv_threshold) cis_divide cis_times_cis_opposite cis_zero
          diff_divide_distrib eq_j minus_real_def mult_1 times_divide_eq_left)
    then have P_last:‹P = ?a1*(?a2*?b3 + ?b2)/(?a1-root3)›
      using P_def jjj by (simp add: )
    then have Q_def:‹Q = (?a3*?b1 + ?b3)/(1-?a3*?a1)› (is ‹_=?Q›)
      using f21' j4 Q_inv by(auto simp:field_simps)  
    have n2: ‹1-?a3*?a1 = (?a2 - root3)/?a2›
      by (smt (verit, ccfv_threshold) cis_divide cis_times_cis_opposite cis_zero
          diff_divide_distrib eq_j minus_real_def mult_1 times_divide_eq_left)
    then have Q_last:‹Q = ?a2*(?a3*?b1 + ?b3)/(?a2-root3)›
      using Q_def jjj by simp
    then have R_def:‹R = (?a1*?b2 + ?b1)/(1-?a1*?a2)› (is ‹_=?R›)
      using f21'' j5 R_inv by(auto simp:field_simps) 
    have n3:‹1-?a1*?a2 = (?a3 - root3)/?a3›
      by (smt (verit, ccfv_threshold) cis_divide cis_times_cis_opposite cis_zero
          diff_divide_distrib eq_j minus_real_def mult_1 times_divide_eq_left)
    then have R_last:‹R = ?a3*(?a1*?b2 + ?b1)/(?a3-root3)›
      using R_def jjj by simp
    have ‹?a1 - root3 ≠ 0 ∧ ?a2-root3≠0 ∧ ?a3-root3 ≠ 0›
      using eq_j j3 j4 j5 by auto
    have rule_s:‹c ≠ 0 ==> a/c + b/c = (a+b)/c› for a b c::real
      by argo
    define j' where 
      defs: ‹j'≡root3›
    have simp_rules_for_eq:‹P = (?a2*?b3 + ?b2)/(1-?a2*?a3)› ‹R = (?a1*?b2 + ?b1)/(1-?a1*?a2)›
      ‹Q = (?a3*?b1 + ?b3)/(1-?a1*?a3)› ‹1-?a1*?a2 ≠ 0 ∧ 1-?a2*?a3≠0 ∧ 1-?a1*?a3 ≠ 0›
      ‹?a1*?a2*?a3 = j' ›
      ‹1 + j' +j'^2 = 0› ‹((1 - ?a1 * ?a3) * ((1 - ?a1 * ?a2) * (1 - ?a2 * ?a3)))≠0›
      ‹j'^3 = 1› ‹j'*j'*j' = 1› ‹?a1≠0› ‹?a2≠0› ‹?a3≠0›
      ‹(1-?a1*?a2)*?a3 = (?a3-j')› ‹(1-?a2*?a3)*?a1 = (?a1-j')› ‹(1-?a1*?a3)*?a2 = (?a2-j')›
      using Q_def P_def R_def eq_j j3 jjj j4 j5 root3_eq_0  root_unity_3  n1 n2 n3 
      by(auto simp add:mult.commute power3_eq_cube defs root3_def)   
    have graal:‹(?a1^2+?a1+1)*?b1 + ?a1^3*(?a2^2+?a2+1)*?b2 +?a1^3*?a2^3*(?a3^2+?a3+1)*?b3 =
 -j'*?a1^2*?a2*(?a1-j')*(?a2-j')*(?a3-j')*(?R +j'*?P +j'^2*?Q)›
      using root_unity_carac[of ?a1 ?a2 ?a3 j' ?R ?b2 ?b1 ?P ?b3 ?Q]
      using simp_rules_for_eq  defs by(auto simp:) 
    then have ‹(?a1^2+?a1+1)*?b1 + ?a1^3*(?a2^2+?a2+1)*?b2 +?a1^3*?a2^3*(?a3^2+?a3+1)*?b3 = 0›
      unfolding defs using very_imp by auto
    then have ‹(?R +j'*?P +j'^2*?Q) = 0›
      using graal simp_rules_for_eq(13) simp_rules_for_eq(14) 
        simp_rules_for_eq(15) simp_rules_for_eq(11) simp_rules_for_eq(12) simp_rules_for_eq(4) by force
    then have impp:‹R +j'*P +j'^2*Q = 0›
      using R_def P_def Q_def 
      by (metis simp_rules_for_eq(1) simp_rules_for_eq(2) )
    have neq_all:‹A≠B ∧ B≠C ∧ C≠A›
      using ‹A ≠ B ∧ R ∉ line A B› ‹A ≠ C ∧ Q ∉ line A C› f2 by argo
    have ‹R ≠ Q›
    proof (rule ccontr)
      assume ‹¬ R ≠ Q›
      then have q1:‹angle_c A B R = angle_c A B Q›
        ‹angle_c B A R = angle_c B A Q› ‹angle_c C A Q = angle_c C A R›
        ‹angle_c A C Q = angle_c A C R›
        using assms by auto
      then have ‹angle_c B A R = ?α› using assms by auto
      then have ‹angle_c B A Q = ?α›
        using q1 by auto
      then have ‹angle_c A B Q = angle_c A B R + angle_c R B Q›
        using ‹¬ R ≠ Q› angle_c_neq0 by auto
      have ‹angle_c C A B = - 3*?α› using assms 
        using ‹angle_c C A Q = - (angle_c B A C / 3)› by argo
      then have ‹angle_c (axial_symmetry B A R) A B = ?α›
        by (metis ‹angle_c (axial_symmetry A B R) A B = angle_c B A C / 3› axial_symmetry_eq)
      have ‹C - A ≠ 0 ∧ Q - A ≠ 0 ∧A - R ≠ 0 ∧ A - B ≠ 0›
        using ‹A ≠ C ∧ Q ∉ line A C› ‹angle_c A B Q = angle_c A B R + angle_c R B Q›
          ‹angle_c R B A = angle_c C B A / 3› neq_0 q1(1) neq_all by fastforce
      then have ‹angle_c C A B = angle_c C A Q + angle_c Q A R + angle_c R A B›
        using angle_c_sum[of C A Q R]  angle_c_sum[of C A R B] 
        by (smt (verit) ‹¬ R ≠ Q› ‹angle_c C A B = - 3 * (angle_c B A C / 3)›
            ‹angle_c C A Q = - (angle_c B A C / 3)› ‹angle_c R A B = - (angle_c B A C / 3)›
            angle_c_neq0 canon_ang(1) canon_ang(2) canon_ang_id)
      then show False 
        using ‹¬ R ≠ Q›
        by (smt (verit, best) ‹angle_c C A B = - 3 * (angle_c B A C / 3)›
            ‹angle_c C A Q = - (angle_c B A C / 3)› ‹angle_c R A B = - (angle_c B A C / 3)›
            angle_c_neq0 neq_0 zero_canonical)
    qed
    then have ‹cdist R P = cdist R Q ∧ cdist R Q = cdist Q P›
      using equilateral_caracterization_neg[of R Q P] impp unfolding defs 
      by (metis cdist_commute)
    then have ?thesis 
      using cdist_commute by auto
  }note case_pi3=this
  then show ?thesis using hhh by auto
qed

theorem Morley_neg: 
  assumes‹¬collinear A B C›
    ‹angle_c A B R = angle_c A B C / 3› (is ‹?abr = ?abc›)
    "angle_c B A R = angle_c B A C / 3" (is ‹?bar = ?α›)
    "angle_c B C P = angle_c B C A / 3" (is ‹?bcp = ?bca›)
    "angle_c C B P = angle_c C B A / 3" (is ‹?cbp = ?β›)
    "angle_c C A Q = angle_c C A B / 3" (is ‹?caq = ?cab›)
    "angle_c A C Q = angle_c A C B / 3" (is ‹?acq = ?γ›)
    and hhh:‹⇂angle_c B A C / 3+angle_c C B A / 3+angle_c A C B / 3⇃ = -pi/3›
  shows  ‹cdist R P = cdist P Q ∧ cdist Q R = cdist P Q›
proof -
  have ‹⇂-angle_c B A C / 3+-angle_c C B A / 3+-angle_c A C B / 3⇃ = pi/3›
    using hhh 
    by (metis (no_types, opaque_lifting) canon_ang(1) canon_ang_uminus less_eq_real_def 
        linorder_not_le minus_add_distrib minus_divide_left mult_le_0_iff  
        nonzero_mult_div_cancel_left not_numeral_le_zero pi_gt_zero times_divide_eq_right verit_minus_simplify(4) zero_canonical)
  then show ?thesis using Morley_pos[of C B A P Q R] 
    by (smt (verit, best) Morley_pos angle_c_commute assms(1) assms(2) assms(3) assms(4) assms(5)
        assms(6) assms(7) cdist_commute collinear_sin_neq_0 collinear_sym1 collinear_sym2 sin_pi)
qed

theorem Morley:
  assumes‹¬collinear A B C›
    ‹angle_c A B R = angle_c A B C / 3› (is ‹?abr = ?abc›)
    "angle_c B A R = angle_c B A C / 3" (is ‹?bar = ?α›)
    "angle_c B C P = angle_c B C A / 3" (is ‹?bcp = ?bca›)
    "angle_c C B P = angle_c C B A / 3" (is ‹?cbp = ?β›)
    "angle_c C A Q = angle_c C A B / 3" (is ‹?caq = ?cab›)
    "angle_c A C Q = angle_c A C B / 3" (is ‹?acq = ?γ›)
  shows  ‹cdist R P = cdist P Q ∧ cdist Q R = cdist P Q›
proof -
  {fix A B C γ
    assume ABC_nline:‹A ∉ line B C›
      and eq_3c:‹angle_c A C B = 3*γ›
    then have neq_PI:‹abs γ < pi/3›
    proof - 
      have ‹angle_c A C B ≠ pi› using ABC_nline(1) unfolding line_def 
        by (metis angle_c_commute_pi collinear_iff mem_Collect_eq non_collinear_independant)
      then have ‹angle_c A C B ∈ {-pi<..<pi}›
        using ang_c_in less_eq_real_def by auto
      then show ‹abs γ < pi/3›
        using eq_3c by force
    qed}note ang_inf_pi3=this
  have ‹⇂angle_c B A C + angle_c C B A + angle_c A C B⇃ = pi›
    by (metis Elementary_Complex_Geometry.collinear_def add.commute 
        angle_sum_triangle_c assms(1) collinear_sym1 collinear_sym2')
  have eq_pi:‹⇂3*?α + 3*?β + 3*?γ⇃ = pi›
    using ‹⇂angle_c B A C + angle_c C B A + angle_c A C B⇃ = pi› by force
  have ‹A∉line B C ∧ B∉ line A C ∧ C ∉ line A B›
    using assms(1) unfolding line_def using collinear_sym1 collinear_sym2' by(auto) 
  then have f2:‹abs ?α < pi/3 ∧ abs ?β < pi/3 ∧ abs ?γ < pi/3›
    using ang_inf_pi3 
    by (smt (verit, ccfv_SIG) ang_vec_bounded angle_c_def assms(1) collinear_sin_neq_0 
        collinear_sym1 collinear_sym2 divide_less_cancel minus_divide_left sin_pi)
  have possi_abc:‹⇂?α+?β+?γ⇃ =pi/3 ∨ ⇂?α+?β+?γ⇃ = -pi/3›
  proof -
    have ‹?α+?β+?γ ≤ pi›
      using f2 by(auto simp:field_simps)
    then have ‹⇂?α+?β+?γ⇃ = ?α+?β+?γ›
      using canon_ang_id f2 by fastforce
    then have ‹⇂3*⇂?α+?β+?γ⇃⇃ = pi›
      using eq_pi by force
    then show ?thesis 
      by (smt (verit) add_divide_distrib arccos_minus_one_half arccos_one_half arcsin_minus_one_half
 arcsin_one_half arcsin_plus_arccos canon_ang_id canon_ang_minus_3pi_minus_pi canon_ang_pi_3pi 
 eq_pi f2 field_sum_of_halves)
  qed
  then show ?thesis 
    using Morley_neg Morley_pos assms(1) assms(2) assms(3) assms(4) assms(5) assms(6) assms(7) 
    by meson
qed

end