Theory Hilbert_Neutral

(* IsageoCoq - Hilbert_Neutral.thy
Port part of GeoCoq 3.4.0 (https://geocoq.github.io/GeoCoq/)

Version 2.0.0 IsaGeoCoq
Copyright (C) 2021-2025 Roland Coghetto roland.coghetto ( a t ) cafr-msa2p.be

History
Version 1.0.0 IsaGeoCoq
Port part of GeoCoq 3.4.0 (https://geocoq.github.io/GeoCoq/) in Isabelle/Hol (Isabelle2021)
Copyright (C) 2021  Roland Coghetto roland_coghetto (at) hotmail.com

License: LGPL

This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 2.1 of the License, or (at your option) any later version.

This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
Lesser General Public License for more details.

You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301  USA
*)

theory Hilbert_Neutral

imports
  Tarski_Neutral

begin

section "Hilbert - Geometry - neutral dimension less"

subsection "Axioms"

locale Hilbert_neutral_dimensionless_pre =
  fixes
    IncidL :: "'p ⇒ 'b ⇒ bool" and
    IncidP :: "'p ⇒ 'c ⇒ bool" and
    EqL ::"'b ⇒ 'b ⇒ bool" and
    EqP ::"'c ⇒ 'c ⇒ bool" and
    IsL ::"'b ⇒ bool" and
    IsP ::"'c ⇒ bool" and
    BetH ::"'p⇒'p⇒'p⇒bool" and
    CongH::"'p⇒'p⇒'p⇒'p⇒bool" and
    CongaH::"'p⇒'p⇒'p⇒'p⇒'p⇒'p⇒bool" 

context Hilbert_neutral_dimensionless_pre

begin

subsection "Definitions"

definition ColH :: "'p ⇒ 'p ⇒ 'p ⇒bool" 
  where
    "ColH A B C ≡ (∃ l. IsL l ∧ IncidL A l ∧ IncidL B l ∧ IncidL C l)"

definition IncidLP :: "'b⇒'c⇒bool" where
  "IncidLP l p ≡ IsL l ∧ IsP p ∧ (∀ A. IncidL A l ⟶ IncidP A p)"

definition cut :: "'b⇒'p⇒'p⇒bool" where
  "cut l A B ≡ IsL l ∧ ¬ IncidL A l ∧ ¬ IncidL B l ∧ (∃ I. IncidL I l ∧ BetH A I B)"

definition outH :: "'p⇒'p⇒'p⇒bool" where
  "outH P A B ≡ BetH P A B ∨ BetH P B A ∨ (P ≠ A ∧ A = B)" 

definition disjoint :: 
  "'p⇒'p⇒'p⇒'p⇒bool" where
  "disjoint A B C D ≡ ¬ (∃ P. BetH A P B ∧ BetH C P D)" 

definition same_side :: "'p⇒'p⇒'b⇒bool" where
  "same_side A B l ≡ IsL l ∧ (∃ P. cut l A P ∧ cut l B P)" 

definition same_side' :: 
  "'p⇒'p⇒'p⇒'p⇒bool" where
  "same_side' A B X Y ≡
     X ≠ Y ∧
     (∀ l::'b. (IsL l ∧ IncidL X l ∧ IncidL Y l) ⟶ same_side A B l)" 

definition Para :: "'b ⇒ 'b ⇒bool" where
  "Para l m ≡ IsL l ∧ IsL m ∧ 
              (¬(∃ X. IncidL X l ∧ IncidL X m)) ∧ (∃ p. IncidLP l p ∧ IncidLP m p)"

definition Bet :: "'p⇒'p⇒'p⇒bool" 
  where
    "Bet A B C ≡ BetH A B C ∨ A = B ∨ B = C"

definition Cong :: "'p⇒'p⇒'p⇒'p⇒bool" 
  where
    "Cong A B C D ≡ (CongH A B C D ∧ A ≠ B ∧ C ≠ D) ∨ (A = B ∧ C = D)"

definition ParaP :: "'p⇒'p⇒'p⇒'p⇒bool" 
  where
    "ParaP A B C D ≡ ∀ l m. 
                      IsL l ∧ IsL m ∧ IncidL A l ∧ IncidL B l ∧ IncidL C m ∧ IncidL D m 
                      ⟶ 
                      Para l m"

definition is_line :: "'p ⇒ 'p ⇒ 'b ⇒bool" 
  where
    "is_line A B l ≡ (IsL l ∧ A ≠ B ∧ IncidL A l ∧ IncidL B l)"

definition cut' :: 
  "'p ⇒ 'p ⇒ 'p ⇒ 'p ⇒ bool" 
  where
    "cut' A B X Y ≡ X ≠ Y ∧ (∀ l. (IsL l ∧ IncidL X l ∧ IncidL Y l) ⟶ cut l A B)"

definition Midpoint :: "'p ⇒ 'p ⇒ 'p⇒bool" 
  ("_ Midpoint _ _" [99,99,99] 50)
  where "M Midpoint A B ≡ Bet A M B ∧ Cong A M M B"

end

locale Hilbert_neutral_dimensionless =  Hilbert_neutral_dimensionless_pre IncidL IncidP EqL EqP 
  IsL IsP BetH CongH CongaH
  for
    IncidL :: "'p ⇒ 'b ⇒ bool" and
    IncidP :: "'p ⇒ 'c ⇒ bool" and
    EqL ::"'b ⇒ 'b ⇒ bool" and
    EqP ::"'c ⇒ 'c ⇒ bool" and
    IsL ::"'b ⇒ bool" and
    IsP ::"'c ⇒ bool" and
    BetH ::"'p⇒'p⇒'p⇒bool" and
    CongH::"'p⇒'p⇒'p⇒'p⇒bool" and
    CongaH::"'p⇒'p⇒'p⇒'p⇒'p⇒'p⇒bool" +
  fixes  PP PQ PR :: 'p
  assumes 
    EqL_refl: "IsL l ⟶ EqL l l" and
    EqL_sym: "IsL l1 ∧ IsL l2 ∧ EqL l1 l2 ⟶ EqL l2 l1" and
    EqL_trans: "(EqL l1 l2 ∧ EqL l2 l3) ⟶ EqL l1 l3" and
    EqP_refl: "IsP p ⟶ EqP p p" and
    EqP_sym: "EqP p1 p2 ⟶ EqP p2 p1" and
    EqP_trans: "(EqP p1 p2 ∧ EqP p2 p3) ⟶ EqP p1 p3" and
    IncidL_morphism: "(IsL l ∧ IsL m ∧  IncidL P l ∧ EqL l m) ⟶ IncidL P m" and
    IncidP_morphism: "(IsP p ∧ IsP q ∧ IncidP M p ∧ EqP p q) ⟶ IncidP M q" and
    Is_line:"IncidL P l ⟶ IsL l" and
    Is_plane:"IncidP P p ⟶ IsP p" 
  assumes
    (** Group I Incidence *)
    line_existence: "A ≠ B ⟶ (∃ l. IsL l ∧ ( IncidL A l ∧ IncidL B l))" and
    line_uniqueness: "A ≠ B ∧ IsL l ∧ IsL m ∧
     IncidL A l ∧ IncidL B l ∧ IncidL A m ∧ IncidL B m ⟶
     EqL l m" and
    two_points_on_line: "∀ l. IsL l ⟶ (∃ A B. IncidL A l ∧ IncidL B l ∧ A ≠ B)" 
  assumes 
    lower_dim_2: "PP ≠ PQ ∧ PQ ≠ PR ∧ PP ≠ PR ∧ ¬ ColH PP PQ PR" and
    (*lower_dim_2: "∃ PP PQ PR. PP ≠ PQ ∧ PQ ≠ PR ∧ PP ≠ PR ∧ ¬ ColH PP PQ PR" and*)
    plan_existence: "∀ A B C. ((¬ ColH A B C) ⟶ 
                               (∃ p. IsP p ∧ IncidP A p ∧ IncidP B p ∧ IncidP C p))" and
    one_point_on_plane: "∀ p. ∃ A. IsP p ⟶ IncidP A p" and
    plane_uniqueness: "¬ ColH A B C ∧ IsP p ∧ IsP q ∧
     IncidP A p ∧ IncidP B p ∧ IncidP C p ∧ IncidP A q ∧ IncidP B q ∧ IncidP C q ⟶
     EqP p q"  and
    line_on_plane: "∀ A B l p. A ≠ B ∧ IsL l ∧ IsP p ∧
     IncidL A l ∧ IncidL B l ∧ IncidP A p ∧ IncidP B p ⟶ IncidLP l p"
  assumes 
    between_diff: "BetH A B C ⟶ A ≠ C" and
    between_col: "BetH A B C ⟶ ColH A B C" and
    between_comm: "BetH A B C ⟶ BetH C B A" and
    between_out: " A ≠ B ⟶ (∃ C. BetH A B C)" and
    between_only_one: "BetH A B C ⟶ ¬ BetH B C A" and
    pasch: "¬ ColH A B C ∧ IsL l ∧ IsP p ∧
     IncidP A p ∧ IncidP B p ∧ IncidP C p ∧ IncidLP l p ∧ ¬ IncidL C l ∧
 (cut l A B)
⟶
     (cut l A C) ∨ (cut l B C)"
  assumes
    cong_permr: "CongH A B C D ⟶ CongH A B D C" and
    cong_existence: "⋀A B A' P::'p. A ≠ B ∧ A' ≠ P ∧ IsL l ∧
     IncidL A' l ∧ IncidL P l ⟶
     (∃ B'. (IncidL B' l ∧ outH A' P B' ∧ CongH A' B' A B))" and
    cong_pseudo_transitivity:
    " CongH A B C D ∧ CongH A B E F ⟶ CongH C D E F" and
    addition : "
     ColH A B C ∧ ColH A' B' C' ∧
     disjoint A B B C ∧ disjoint A' B' B' C' ∧
     CongH A B A' B' ∧ CongH B C B' C' ⟶
     CongH A C A' C'" and
    conga_refl: "¬ ColH A B C ⟶ CongaH A B C A B C" and
    conga_comm : "¬ ColH A B C ⟶ CongaH A B C C B A" and
    conga_permlr: "CongaH A B C D E F ⟶ CongaH C B A F E D" and
    conga_out_conga: "(CongaH A B C D E F ∧
    outH B A A' ∧ outH B C C' ∧ outH E D D' ∧ outH E F F') ⟶
    CongaH A' B C' D' E F'" and
    cong_4_existence: 
    " ¬ ColH P PO X ∧ ¬ ColH A B C ⟶
            (∃ Y. (CongaH A B C X PO Y ∧ same_side' P Y PO X))" and
    cong_4_uniqueness:
    "¬ ColH P PO X ∧ ¬ ColH A B C ∧
     CongaH A B C X PO Y ∧ CongaH A B C X PO Y' ∧
     same_side' P Y PO X ∧ same_side' P Y' PO X ⟶
     outH PO Y Y'" and
    cong_5 : "¬ ColH A B C ∧ ¬ ColH A' B' C' ∧
     CongH A B A' B' ∧ CongH A C A' C' ∧
     CongaH B A C B' A' C' ⟶
     CongaH A B C A' B' C'"

context Hilbert_neutral_dimensionless

begin

subsection "Propositions"


lemma betH_distincts: 
  assumes "BetH A B C"
  shows "A ≠ B ∧ B ≠ C ∧ A ≠ C" 
  using assms between_comm between_diff between_only_one by blast

(** Hilbert's congruence is 'defined' only for non degenerated segments,
while Tarski's segment congruence allows the null segment. *)

lemma congH_perm: 
  assumes "A ≠ B"
  shows "CongH A B B A"
proof -
  obtain l where "IsL l" and "IncidL A l" and "IncidL B l"
    using assms line_existence by fastforce
  moreover
  {
    fix x
    assume "IncidL x l" and 
      "outH A B x" and 
      "CongH A x A B"
    hence "CongH A x B A" 
      by (simp add: cong_permr)
    hence "CongH A B B A" 
      using ‹CongH A x A B› cong_pseudo_transitivity by blast
  }
  hence "∀ x. (IncidL x l ∧ outH A B x ∧ CongH A x A B) ⟶ CongH A B B A" 
    by blast
  ultimately show ?thesis 
    using assms cong_existence by presburger
qed

lemma congH_refl: 
  assumes "A ≠ B" 
  shows "CongH A B A B" 
  by (simp add: assms congH_perm cong_permr)

lemma congH_sym: 
  assumes "A ≠ B" and
    "CongH A B C D"
  shows "CongH C D A B" 
  using assms(1) assms(2) congH_refl cong_pseudo_transitivity by blast

lemma colH_permut_231: 
  assumes "ColH A B C"
  shows "ColH B C A" 
  using ColH_def assms by blast

lemma colH_permut_312:
  assumes "ColH A B C"
  shows "ColH C A B" 
  by (simp add: assms colH_permut_231)

lemma colH_permut_213:
  assumes "ColH A B C"
  shows "ColH B A C" 
  using ColH_def assms by auto

lemma colH_permut_132:
  assumes "ColH A B C"
  shows "ColH A C B" 
  using ColH_def assms by auto

lemma colH_permut_321:
  assumes "ColH A B C"
  shows "ColH C B A" 
  using ColH_def assms by auto

lemma other_point_exists: 
  fixes A::'p
  shows "∃ B. A ≠ B" 
  by (metis lower_dim_2)

lemma colH_trivial111:
  shows "ColH A A A" 
  using cong_4_existence same_side'_def by blast

lemma colH_trivial112:
  shows "ColH A A B" 
  using colH_permut_231 cong_4_existence same_side'_def by blast

lemma colH_trivial122:
  shows "ColH A B B" 
  by (simp add: colH_permut_312 colH_trivial112)

lemma colH_trivial121:
  shows "ColH A B A" 
  by (simp add: colH_permut_312 colH_trivial122)

lemma colH_dec:
  shows "ColH A B C ∨ ¬ ColH A B C" 
  by blast

lemma colH_trans:
  assumes "X ≠ Y" and
    "ColH X Y A" and
    "ColH X Y B" and
    "ColH X Y C"
  shows "ColH A B C"
proof -
  obtain l where "IsL l" and "IncidL X l" and "IncidL Y l" and "IncidL A l" 
    using ColH_def assms(2) by blast
  obtain m where "IsL m" and "IncidL X m" and "IncidL Y m" and "IncidL B m" 
    using ColH_def assms(3) by blast
  obtain n where "IsL n" and "IncidL X n" and "IncidL Y n" and "IncidL C n" 
    using ColH_def assms(4) by blast
  have "EqL l m" 
    using line_uniqueness ‹IncidL B m› assms(1) ‹IncidL X l› ‹IncidL Y l› 
      ‹IncidL X m› ‹IncidL Y m› ‹IsL m› ‹IsL l› by blast
  hence "IncidL B l" 
    using EqL_sym IncidL_morphism ‹IncidL B m› ‹IsL l› ‹IsL m› by blast
  moreover have "IncidL C l"   
    by (meson IncidL_morphism ‹IncidL C n› ‹IncidL X l› ‹IncidL X n› ‹IncidL Y l›
        ‹IncidL Y n› ‹IsL l› ‹IsL n› assms(1) line_uniqueness)
  ultimately show ?thesis
    using ColH_def ‹IncidL A l› ‹IsL l› by blast
qed

lemma bet_colH:
  assumes "Bet A B C" 
  shows "ColH A B C" 
  using Bet_def assms between_col colH_trivial112 colH_trivial122 by blast

lemma ncolH_exists: 
  assumes "A ≠ B"
  shows "∃ C. ¬ ColH A B C" 
  using assms colH_trans lower_dim_2 by blast

lemma ncolH_distincts: 
  assumes "¬ ColH A B C"
  shows "A ≠ B ∧ B ≠ C ∧ A ≠ C" 
  using assms colH_trivial112 colH_trivial121 colH_trivial122 by blast

lemma betH_expand: 
  assumes "BetH A B C" 
  shows "BetH A B C ∧ A ≠ B ∧ B ≠ C ∧ A ≠ C ∧ ColH A B C" 
  using assms betH_distincts between_col by presburger

lemma inter_uniquenessH: 
  assumes "A' ≠ B'" and
    "¬ ColH A B A'" and
    "ColH A B X" and
    "ColH A B Y" and
    "ColH A' B' X" and
    "ColH A' B' Y"
  shows "X = Y"
proof -
  have "A ≠ B" 
    using assms(2) colH_trivial112 by blast
  thus ?thesis
    by (metis (full_types) assms(1) assms(2) assms(3) assms(4) assms(5) assms(6) 
        colH_permut_231 colH_trans colH_trivial121)
qed

lemma inter_incid_uniquenessH:
  assumes "¬ IncidL P l" and
    "IncidL P m" and 
    "IncidL X l" and
    "IncidL Y l" and
    "IncidL X m" and
    "IncidL Y m"
  shows "X = Y" 
proof -
  have "IsL l" 
    using Is_line assms(4) by blast
  then  obtain A B where "IncidL B l" and "IncidL A l" and "A ≠ B" 
    using two_points_on_line by blast
  have "IsL m" 
    using Is_line assms(5) by blast
  then obtain A' B' where "IncidL B' m" and "IncidL A' m" and "A' ≠ B'"
    using two_points_on_line by blast
  have "ColH A B X" 
    using ColH_def Is_line ‹IncidL A l› ‹IncidL B l› assms(3) by blast
  have "ColH A B Y" 
    using ColH_def Is_line ‹IncidL A l› ‹IncidL B l› assms(4) by blast
  have "ColH A' B' X" 
    using ColH_def Is_line ‹IncidL A' m› ‹IncidL B' m› assms(5) by blast
  have "ColH A' B' Y" 
    using ColH_def Is_line ‹IncidL A' m› ‹IncidL B' m› assms(6) by blast
  {
    assume "ColH A B P"
    then obtain l00 where "IsL l00" and "IncidL A l00" and "IncidL B l00" and "IncidL P l00" 
      using ColH_def by blast
    hence "EqL l l00" 
      using ‹A ≠ B› ‹IncidL A l› ‹IncidL B l› ‹IsL l› line_uniqueness by blast
    hence "IncidL P l" 
      using EqL_sym IncidL_morphism ‹IncidL P l00› ‹IsL l00› ‹IsL l› by blast
    hence False 
      using assms(1) by blast
  }
  hence "¬ ColH A B P" 
    by blast
  {
    assume "A' = P"
    hence "X = Y" 
      using ‹A' ≠ B'› ‹ColH A B X› ‹ColH A B Y› ‹ColH A' B' X› ‹ColH A' B' Y› ‹¬ ColH A B P› 
        inter_uniquenessH by blast
  }
  moreover
  {
    assume "A' ≠ P"
    hence "X = Y" 
      using IncidL_morphism ‹IsL l› ‹IsL m› assms(1) assms(2) assms(3) assms(4) assms(5) 
        assms(6) line_uniqueness by blast
  }
  ultimately show ?thesis 
    by blast
qed

lemma between_only_one': 
  assumes "BetH A B C" (*and
"¬ BetH B C A"*)
  shows "¬ BetH B A C" 
  using assms(1) between_comm between_only_one by blast

lemma betH_colH: 
  assumes "BetH A B C"
  shows "ColH A B C ∧ A ≠ B ∧ B ≠ C ∧ A ≠ C" 
  using assms betH_expand by presburger

lemma cut_comm: 
  assumes "cut l A B"
  shows "cut l B A" 
  using assms between_comm local.cut_def by blast

lemma line_on_plane': 
  assumes "A ≠ B" and
    "IncidP A p" and 
    "IncidP B p" and
    "ColH A B C"
  shows "IncidP C p" 
  using ColH_def IncidLP_def Is_plane assms(1) assms(2) assms(3) assms(4) line_on_plane by blast

lemma inner_pasch_aux:
  assumes "¬ ColH B C P" and
    "Bet A P C" and
    "Bet B Q C"
  shows "∃ X. Bet P X B ∧ Bet Q X A" 
proof -
  have "BetH A P C ∨ A = P ∨ P = C" 
    using Bet_def assms(2) by presburger
  moreover
  have "BetH B Q C ∨ B = Q ∨ Q = C" 
    using Bet_def assms(3) by blast
  moreover
  let ?t = "∃ X. Bet P X B ∧ Bet Q X A"
  have "BetH A P C ∧ BetH B Q C ⟶ ?t"
  proof -
    {
      assume "Q ≠ A" and
        "BetH A P C" and "BetH B Q C"
      obtain l where "IsL l" and "IncidL Q l" and "IncidL A l" 
        using ‹Q ≠ A› line_existence by blast
      {
        assume "P = A"
        hence ?t 
          using Bet_def by blast
      }
      moreover
      {
        assume "P ≠ A"
        {
          assume "Q = C"
          hence ?t 
            using ‹BetH B Q C› betH_distincts by auto
        }
        moreover
        {
          assume "Q ≠ C"
          {
            assume "IncidL P l"
            have "ColH A P C" 
              using ‹BetH A P C› betH_colH by blast
            have "ColH B Q C" 
              by (simp add: ‹BetH B Q C› between_col)
            have "ColH A P Q" 
              using ColH_def ‹IncidL A l› ‹IncidL P l› ‹IncidL Q l› ‹IsL l› by blast
            have "ColH P C Q" 
              by (meson ColH_def ‹ColH A P C› ‹IncidL A l› ‹IncidL P l› ‹IncidL Q l› 
                  ‹P ≠ A› inter_incid_uniquenessH)
            have "ColH B C P" 
              by (metis inter_uniquenessH ‹ColH B Q C› ‹ColH P C Q› ‹Q ≠ C› 
                  colH_permut_321 colH_trivial122)
            hence False 
              using assms(1) by blast
          }
          hence "¬ IncidL P l" 
            by blast
          {
            assume "B = Q"
            hence ?t 
              using Bet_def by blast
          }
          moreover
          {
            assume "B ≠ Q"
            {
              assume "A = C"
              hence ?t 
                using ‹BetH A P C› between_diff by blast
            }
            moreover
            {
              assume "A ≠ C"
              {
                assume "IncidL B l"
                have "ColH A B Q" 
                  using ColH_def ‹IncidL A l› ‹IncidL B l› ‹IncidL Q l› ‹IsL l› by blast
                have "ColH A B C" 
                  using ‹BetH B Q C› ‹ColH A B Q› betH_colH colH_permut_231 colH_trans 
                    colH_trivial121 by blast
                have "ColH A P C" 
                  by (simp add: ‹BetH A P C› betH_colH)
                have "ColH B Q C" 
                  by (simp add: ‹BetH B Q C› between_col)
                have "ColH B C P" 
                  by (meson ColH_def ‹A ≠ C› ‹ColH A B C› ‹ColH A P C› inter_incid_uniquenessH)
                hence False 
                  using assms(1) by blast
              }
              hence "¬ IncidL B l" 
                by blast
              {
                assume "IncidL C l"
                have "ColH A C Q" 
                  using ColH_def ‹IncidL A l› ‹IncidL C l› ‹IncidL Q l› ‹IsL l› by blast
                have "ColH B Q C" 
                  using assms(3) bet_colH by auto
                have "ColH A B C" 
                  by (metis ‹BetH B Q C› ‹ColH A C Q› ‹Q ≠ C› betH_colH colH_permut_231 
                      colH_trans colH_trivial121)
                have "ColH B C P" 
                  using inter_incid_uniquenessH ColH_def ‹A ≠ C› ‹ColH A B C› ‹IncidL A l› 
                    ‹IncidL C l› ‹¬ IncidL B l› by fastforce
                hence False 
                  by (simp add: assms(1))
              }
              have "cut l B C" 
                using ‹BetH B Q C› ‹IncidL C l ⟹ False› ‹IncidL Q l› ‹IsL l› ‹¬ IncidL B l› 
                  local.cut_def by blast
              obtain p where "IncidP B p" and "IncidP C p" and "IncidP P p" 
                using assms(1) plan_existence by blast
              have "(¬ ColH B C P ∧ IncidP B p ∧ IncidP C p ∧ IncidP P p ∧ IncidLP l p ∧
                         ¬ IncidL P l ∧ cut l B C) ⟶ cut l B P ∨ cut l C P" 
                using pasch Is_plane ‹IsL l› by blast
              moreover
              have "¬ ColH B C P" 
                by (simp add: assms(1))
              moreover have "IncidP B p" 
                by (simp add: ‹IncidP B p›)
              moreover have "IncidP C p" 
                by (simp add: ‹IncidP C p›)
              moreover have "IncidP P p" 
                by (simp add: ‹IncidP P p›)
              moreover have "IncidLP l p" 
                by (metis colH_permut_231 line_on_plane' 
                    Hilbert_neutral_dimensionless.ncolH_distincts 
                    Hilbert_neutral_dimensionless_axioms Is_plane ‹IncidL A l› ‹IncidL Q l› 
                    ‹IsL l› ‹Q ≠ A› assms(2) assms(3) bet_colH calculation(2) calculation(3) 
                    calculation(4) calculation(5) line_on_plane)
              moreover have "¬ IncidL P l" 
                by (simp add: ‹¬ IncidL P l›)
              moreover have "cut l B C" 
                by (simp add: ‹local.cut l B C›)
              moreover
              {
                assume "cut l B P"
                hence "¬ IncidL B l" 
                  using ‹¬ IncidL B l› by auto
                have "¬ IncidL P l" 
                  by (simp add: calculation(7))
                obtain X where "IncidL X l" and "BetH B X P" 
                  using ‹local.cut l B P› local.cut_def by blast
                have "BetH P X B ∨ P = X ∨ X = B" 
                  using ‹BetH B X P› between_comm by presburger
                moreover have "BetH Q X A ∨ Q = X ∨ X = A"
                proof (cases "A = X")
                  case True
                  thus ?thesis 
                    by simp
                next
                  case False
                  have "A ≠ Q" 
                    using ‹Q ≠ A› by fastforce
                  have "P ≠ C" 
                    using assms(1) colH_trivial122 by blast
                  have "A ≠ B" 
                    using ‹IncidL A l› ‹¬ IncidL B l› by auto
                  have "X ≠ Q" 
                    using ‹B ≠ Q› ‹BetH B X P› assms(1) assms(3) bet_colH between_col 
                      colH_trans colH_trivial121 by blast
                  have "ColH A X Q" 
                    using ColH_def Is_line ‹IncidL A l› ‹IncidL Q l› ‹IncidL X l› by blast
                  {
                    assume "ColH A C Q"
                    obtain l00 where "IncidL A l00" and "IncidL C l00" and "IncidL Q l00" 
                      using ColH_def ‹ColH A C Q› by blast
                    hence "IncidL C l" 
                      using ‹A ≠ Q› ‹IncidL A l› ‹IncidL Q l› inter_incid_uniquenessH by blast
                    hence False 
                      using ‹IncidL C l ⟹ False› by auto
                  }
                  hence "¬ ColH A C Q" 
                    by blast
                  have "P ≠ B" 
                    using assms(1) colH_trivial121 by fastforce
                  obtain m where "IsL m" and "IncidL P m" and "IncidL B m" 
                    using ‹P ≠ B› line_existence by blast
                  have "¬ IncidL Q m" 
                    by (meson ColH_def ‹B ≠ Q› ‹BetH B Q C› ‹IncidL B m› ‹IncidL P m› assms(1)
                        between_col inter_incid_uniquenessH)
                  have "¬ ColH A B P" 
                    by (metis ‹BetH A P C› ‹P ≠ A› assms(1) betH_colH colH_permut_312 
                        colH_trans colH_trivial122)
                  have "cut m A C" 
                    using Hilbert_neutral_dimensionless_pre.ColH_def ‹BetH A P C› 
                      ‹IncidL B m› ‹IncidL P m› ‹IsL m› ‹¬ ColH A B P› assms(1) 
                      local.cut_def by fastforce
                  obtain p where "IncidP A p" and "IncidP C p" and "IncidP Q p" 
                    using ‹¬ ColH A C Q› plan_existence by blast
                  have "(¬ ColH A C Q ∧ IncidP A p ∧ IncidP C p ∧ IncidP Q p ∧
                           IncidLP m p ∧ ¬ IncidL Q m ∧ cut m A C) ⟶ (cut m A Q ∨ cut m C Q)" 
                    using pasch Is_plane ‹IsL m› by blast
                  moreover have "¬ ColH A C Q ∧ IncidP A p ∧ IncidP C p ∧ IncidP Q p ∧
                           IncidLP m p ∧ ¬ IncidL Q m ∧ cut m A C" 
                    by (metis Is_plane ‹A ≠ C› ‹BetH A P C› ‹BetH B Q C› ‹IncidL B m› 
                        ‹IncidL P m› ‹IncidP A p› ‹IncidP C p› ‹IncidP Q p›
                        ‹IsL m› ‹P ≠ B› ‹Q ≠ C›
                        ‹¬ ColH A C Q› ‹¬ IncidL Q m› ‹local.cut m A C› between_col between_comm 
                        colH_permut_132 line_on_plane line_on_plane')
                  moreover {
                    assume "cut m A Q"
                    obtain Y where "IncidL Y m ∧ BetH A Y Q" 
                      using ‹local.cut m A Q› local.cut_def by blast
                    have "ColH A Y Q" 
                      by (simp add: ‹IncidL Y m ∧ BetH A Y Q› betH_colH)
                    then obtain l0 where "IncidL A l0" and "IncidL Y l0" and "IncidL Q l0" 
                      using ColH_def by blast
                    have "EqL l0 l" 
                      using Is_line ‹A ≠ Q› ‹IncidL A l0› ‹IncidL A l› ‹IncidL Q l0›
                        ‹IncidL Q l› line_uniqueness by presburger
                    hence "IncidL Y l" 
                      using ‹A ≠ Q› ‹IncidL A l0› ‹IncidL A l› ‹IncidL Q l0› ‹IncidL Q l›
                        ‹IncidL Y l0› inter_incid_uniquenessH by blast
                    moreover
                    have "ColH B X P" 
                      by (simp add: ‹BetH B X P› between_col)
                    then obtain m0 where "IncidL B m0" and "IncidL X m0" and "IncidL P m0" 
                      using ColH_def by blast
                    have "EqL m0 m" 
                      using Is_line ‹IncidL B m0› ‹IncidL B m› ‹IncidL P m0› ‹IncidL P m›
                        ‹P ≠ B› line_uniqueness by presburger
                    hence "IncidL X m" 
                      using IncidL_morphism Is_line ‹IncidL X m0› ‹IsL m› by blast
                    ultimately
                    have "X = Y"
                      using ‹IncidL B m› ‹IncidL X l› ‹IncidL Y m ∧ BetH A Y Q›
                        ‹¬ IncidL B l› inter_incid_uniquenessH by auto
                    hence ?thesis 
                      using ‹IncidL Y m ∧ BetH A Y Q› between_comm by blast
                  }
                  moreover {
                    assume "cut m C Q"
                    then obtain I where "IncidL I m" and "BetH C I Q" 
                      using local.cut_def by blast
                    have "ColH C I Q" 
                      using ‹BetH C I Q› betH_colH by blast
                    obtain lo where "IncidL C lo" and "IncidL I lo" and "IncidL Q lo" 
                      using ColH_def ‹ColH C I Q› by auto
                    {
                      assume "IncidL C m"
                      hence "ColH B C P" 
                        using ‹local.cut m A C› local.cut_def by blast
                      hence False 
                        by (simp add: assms(1))
                    }
                    have "IncidL B lo" 
                      using ColH_def ‹BetH B Q C› ‹IncidL C lo› ‹IncidL Q lo› betH_colH
                        inter_incid_uniquenessH by blast
                    have "I = B" 
                      using ‹IncidL B lo› ‹IncidL B m› ‹IncidL I lo› ‹IncidL I m› 
                        ‹IncidL Q lo› ‹¬ IncidL Q m› inter_incid_uniquenessH by blast
                    hence ?thesis 
                      using ‹BetH B Q C› ‹BetH C I Q› between_only_one by blast
                  }
                  ultimately show ?thesis 
                    by blast
                qed
                ultimately have ?t 
                  using Bet_def by auto
              }
              moreover
              {
                assume "cut l C P"
                then obtain I where "IncidL I l" and "BetH C I P" 
                  using local.cut_def by blast
                have "A = I" 
                proof -
                  obtain s where "IncidL A s" and "IncidL C s"
                    using ‹A ≠ C› line_existence by blast
                  {
                    assume "IncidL Q s" 
                    have "A ≠ Q" 
                      using ‹Q ≠ A› by blast
                    have "EqL l s" 
                      using Is_line ‹A ≠ Q› ‹IncidL A l› ‹IncidL A s› ‹IncidL Q l›
                        ‹IncidL Q s› line_uniqueness by presburger
                    hence False 
                      using ‹A ≠ Q› ‹IncidL A l› ‹IncidL A s› ‹IncidL C l ⟹ False›
                        ‹IncidL C s› ‹IncidL Q l› ‹IncidL Q s› inter_incid_uniquenessH by blast
                  }
                  moreover 
                  have "ColH C I P" 
                    by (simp add: ‹BetH C I P› betH_colH)
                  have "ColH A P C" 
                    by (simp add: ‹BetH A P C› betH_colH)
                  then obtain s0 where "IncidL A s0" and "IncidL P s0" and "IncidL C s0" 
                    using ColH_def by blast
                  have "EqL s s0" 
                    using Is_line ‹A ≠ C› ‹IncidL A s0› ‹IncidL A s› ‹IncidL C s0› 
                      ‹IncidL C s› line_uniqueness by presburger
                  obtain s1 where "IsL s1" and "IncidL C s1" and "IncidL I s1" and "IncidL P s1" 
                    using ColH_def ‹ColH C I P› by blast
                  have "EqL s s1" 
                    by (metis EqL_trans Is_line ‹BetH C I P› ‹EqL s s0› ‹IncidL C s0›
                        ‹IncidL C s1› ‹IncidL P s0› ‹IncidL P s1› between_diff line_uniqueness)
                  hence "IncidL I s" 
                    by (meson EqL_sym IncidL_morphism Is_line ‹IncidL C s› ‹IncidL I s1›)
                  ultimately show ?thesis 
                    using ‹IncidL A l› ‹IncidL A s› ‹IncidL I l› ‹IncidL Q l› 
                      inter_incid_uniquenessH by blast
                qed
                hence ?t 
                  using ‹BetH A P C› ‹BetH C I P› between_only_one by blast
              }
              ultimately have ?t 
                by blast
            }
            ultimately have ?t 
              by blast
          }
          ultimately have ?t 
            by blast
        }
        ultimately have ?t 
          by blast
      }
      ultimately have ?t 
        by blast
    }
    moreover
    {
      assume "Q = A" and
        "BetH A P C" and 
        "BetH B Q C"
      have False
        by (metis (mono_tags, opaque_lifting) ‹BetH A P C› ‹Q = A› assms(1,2,3) bet_colH 
            between_diff colH_permut_231 colH_trans colH_trivial121)
    }
    ultimately show ?thesis 
      by blast
  qed
  moreover have "BetH A P C ∧ B = Q ⟶ ?t" 
    using Bet_def by blast
  moreover have "BetH A P C ∧ Q = C ⟶ ?t" 
    by (meson Bet_def between_comm)
  moreover have "A = P ∧ BetH B Q C ⟶ ?t" 
    using Bet_def by auto
  moreover have "A = P ∧ B = Q ⟶ ?t" 
    using Bet_def by auto
  moreover have "A = P ∧ Q = C ⟶ ?t" 
    using Bet_def by blast
  moreover have "P = C ∧ BetH B Q C ⟶ ?t" 
    using assms(1) colH_trivial122 by blast
  moreover have "P = C ∧ B = Q ⟶ ?t" 
    using assms(1) colH_trivial122 by blast
  moreover have "P = C ∧ Q = C ⟶ ?t" 
    using assms(1) colH_trivial122 by blast
  ultimately show ?thesis
    by blast
qed

lemma betH_trans1:
  assumes "BetH A B C" and
    "BetH B C D"
  shows "BetH A C D" 
proof -
  have "A ≠ B" 
    using assms(1) betH_distincts by blast
  have "C ≠ B" 
    using assms(1) betH_distincts by blast
  have "A ≠ C" 
    using assms(1) betH_expand by blast
  have "D ≠ C" 
    using assms(2) betH_distincts by blast
  have "D ≠ B" 
    using assms(2) between_diff by blast
  obtain E where "¬ ColH A C E" 
    using ‹A ≠ C› ncolH_exists by presburger
  hence "C ≠ E" 
    by (simp add: ncolH_distincts)
  obtain F where "BetH C E F" 
    using ‹C ≠ E› between_out by fastforce
  have "E ≠ F" 
    using ‹BetH C E F› betH_distincts by blast
  have "C ≠ F" 
    using ‹BetH C E F› between_diff by blast
  have "ColH A B C" 
    using assms(1) betH_colH by auto
  have "ColH B C D" 
    by (simp add: assms(2) betH_colH)
  have "ColH C E F" 
    using ‹BetH C E F› between_col by auto
  have "¬ ColH F C B" 
    using ColH_def ‹C ≠ B› ‹C ≠ F› ‹ColH A B C› ‹ColH C E F› ‹¬ ColH A C E› 
      inter_incid_uniquenessH by auto
  have "∃ X. Bet B X F ∧ Bet E X A" 
  proof -
    have "Bet A B C" 
      by (simp add: Bet_def assms(1))
    moreover have "Bet F E C" 
      by (simp add: Bet_def ‹BetH C E F› between_comm)
    ultimately show ?thesis 
      using ‹¬ ColH F C B› inner_pasch_aux by auto
  qed
  then obtain G where "Bet B G F" and "Bet E G A"
    by blast
  {
    assume "BetH B G F"
    hence "ColH B G F" 
      by (simp add: ‹Bet B G F› bet_colH)
    {
      assume "BetH E G A"
      hence "ColH E G A" 
        by (simp add: betH_colH)
      {
        assume "ColH D B G"
        hence "ColH B D F" 
          by (metis betH_colH ‹BetH B G F› colH_permut_231 colH_trans colH_trivial121)
        hence False 
          by (metis ‹ColH B C D› ‹D ≠ B› ‹¬ ColH F C B› colH_permut_132 
              colH_trans colH_trivial121)
      }
      obtain m where "IncidL C m" and "IncidL E m" 
        using ‹C ≠ E› line_existence by blast
      {
        assume "cut m A G ∨ cut m B G" 
        moreover
        {
          assume "cut m A G"
          then obtain E' where "IncidL E' m" and "BetH A E' G" 
            using local.cut_def by blast
          have "E = E'" 
          proof -
            have "C ≠ F"            
              by (simp add: ‹C ≠ F›)
            moreover have "ColH A G E"                 
              by (simp add: ‹ColH E G A› colH_permut_321)
            moreover have "ColH A G E'"                 
              using ‹BetH A E' G› between_col colH_permut_132 by blast
            moreover have "ColH C F E"                 
              by (simp add: ‹ColH C E F› colH_permut_132)
            moreover have "¬ ColH A G C"                 
              by (metis betH_colH ‹BetH A E' G› ‹¬ ColH A C E› calculation(2) 
                  colH_trans colH_trivial121)
            moreover have "ColH C F E'"                 
              by (meson ColH_def ‹C ≠ E› ‹IncidL C m› ‹IncidL E m› ‹IncidL E' m› 
                  calculation(4) inter_incid_uniquenessH)
            ultimately show ?thesis
              using inter_uniquenessH by blast
          qed
          have "¬ Bet E G A" 
            using ‹BetH A E' G› ‹BetH E G A› ‹E = E'› between_only_one by blast
          hence False 
            using ‹Bet E G A› ‹¬ Bet E G A› by blast
        }
        moreover
        {
          assume "cut m B G"
          obtain F' where "IncidL F' m" and "BetH B F' G" 
            using ‹local.cut m B G› local.cut_def by blast
          have "ColH C E F'" 
            using ColH_def Is_line ‹IncidL C m› ‹IncidL E m› ‹IncidL F' m› by blast
          have "B ≠ G" 
            using ‹BetH B F' G› between_diff by auto
          have "¬ ColH C E B" 
            using ‹C ≠ E› ‹ColH C E F› ‹¬ ColH F C B› colH_trans colH_trivial121 by blast
          hence "F = F'"
            using inter_uniquenessH ‹ColH C E F› ‹B ≠ G› ‹BetH B F' G› ‹ColH B G F› 
              ‹ColH C E F'› between_col colH_permut_132 by blast
          hence "¬ BetH F G B" 
            using ‹BetH B F' G› between_only_one by blast
          hence False 
            using ‹BetH B G F› between_comm by blast
        }
        ultimately have False 
          by blast
      }
      hence "¬ (cut m A G ∨ cut m B G)" 
        by blast
      have "¬ ColH B D G" 
        using ‹ColH D B G ⟹ False› colH_permut_213 by blast
      {
        assume "IncidL G m"
        hence "ColH C E G" 
          using ColH_def Is_line ‹IncidL C m› ‹IncidL E m› by blast
        hence "ColH A C E" 
          by (metis betH_colH ‹BetH E G A› colH_permut_231 colH_trans colH_trivial121)
        hence False 
          by (simp add: ‹¬ ColH A C E›)
      }
      hence "¬ IncidL G m" 
        by blast
      {
        assume "IncidL D m"
        have "ColH A C D" 
          by (meson ColH_def ‹C ≠ B› ‹ColH A B C› ‹ColH B C D› inter_incid_uniquenessH)
        hence "ColH A C E" 
          by (meson ColH_def ‹D ≠ C› ‹IncidL C m› ‹IncidL D m› ‹IncidL E m› 
              inter_incid_uniquenessH)
        hence False 
          by (simp add: ‹¬ ColH A C E›)
      }
      hence "¬ IncidL D m" 
        by blast
      {
        assume "IncidL B m"
        hence "ColH A C E" 
          using ColH_def ‹C ≠ B› ‹ColH B C D› ‹IncidL C m› ‹¬ IncidL D m› 
            inter_incid_uniquenessH by blast
        hence False 
          by (simp add: ‹¬ ColH A C E›)
      }
      hence "¬ IncidL B m" 
        by blast
      hence "cut m D B" 
        using Is_line ‹IncidL C m› ‹¬ IncidL D m› assms(2) between_comm 
          local.cut_def by blast
      obtain p where "IncidP B p" and "IncidP D p" and "IncidP G p" 
        using ‹¬ ColH B D G› plan_existence by blast
      have "(¬ ColH B D G ∧ IncidP B p ∧ IncidP D p ∧ IncidP G p ∧ 
                IncidLP m p ∧ ¬ IncidL G m ∧ cut m B D) ⟶ (cut m B G ∨ cut m D G)" 
        using IncidLP_def pasch by blast
      moreover have "¬ ColH B D G ∧ IncidP B p ∧ IncidP D p ∧ IncidP G p ∧ 
                        IncidLP m p ∧ ¬ IncidL G m ∧ cut m B D" 
        by (metis betH_colH Is_line Is_plane ‹BetH B G F› ‹C ≠ E› ‹C ≠ F› ‹ColH B C D›
            ‹ColH C E F› ‹D ≠ B› ‹IncidL C m› ‹IncidL E m› ‹IncidP B p› ‹IncidP D p› 
            ‹IncidP G p› ‹¬ ColH B D G› ‹¬ IncidL G m› ‹local.cut m D B› colH_permut_312 
            cut_comm line_on_plane line_on_plane')
      ultimately have "cut m B G ∨ cut m D G" 
        by blast
      moreover
      {
        assume "cut m B G"
        hence ?thesis 
          using ‹¬ (local.cut m A G ∨ local.cut m B G)› by blast
      }
      moreover
      {
        assume "cut m D G"
        obtain HX where "IncidL HX m" and "BetH D HX G" 
          using ‹local.cut m D G› local.cut_def by auto
        {
          assume "ColH G D A"
          have "ColH A D B" 
            by (metis ‹C ≠ B› ‹ColH A B C› ‹ColH B C D› colH_permut_231 colH_trans 
                colH_trivial121)
          hence False 
            by (metis ‹ColH G D A› ‹¬ ColH B D G› assms(1) assms(2) between_comm 
                between_only_one' colH_permut_321 colH_trans colH_trivial122)
        }
        hence "¬ ColH G D A" 
          by blast
        {
          assume "IncidL A m"
          hence "ColH A C E" 
            using ColH_def ‹A ≠ C› ‹ColH A B C› ‹IncidL C m› ‹¬ IncidL B m› 
              inter_incid_uniquenessH by blast
          hence False 
            by (simp add: ‹¬ ColH A C E›)
        }
        hence "¬ IncidL A m" 
          by blast
        have "cut m G D" 
          by (simp add: ‹local.cut m D G› cut_comm)
        obtain p where "IncidP G p" and "IncidP D p" and "IncidP A p" 
          using ‹¬ ColH G D A› plan_existence by blast
        have "(¬ ColH G D A ∧ IncidP G p ∧ IncidP D p ∧ IncidP A p ∧ 
                IncidLP m p ∧ ¬ IncidL A m ∧ cut m G D)⟶ (cut m G A ∨ cut m D A)" 
          using pasch Is_line Is_plane ‹IncidL HX m› by blast
        moreover
        have "¬ ColH G D A ∧ IncidP G p ∧ IncidP D p ∧ IncidP A p ∧ 
                IncidLP m p ∧ ¬ IncidL A m ∧ cut m G D" 
        proof -
          have "¬ ColH G D A ∧ IncidP G p ∧ IncidP D p ∧ IncidP A p" 
            using ‹IncidP A p› ‹IncidP D p› ‹IncidP G p› ‹¬ ColH G D A› by blast
          moreover 
          have "ColH B D C" 
            by (simp add: ‹ColH B C D› colH_permut_132)
          have "ColH B A D" 
            by (metis ‹C ≠ B› ‹ColH A B C› ‹ColH B C D› colH_permut_231 
                colH_trans colH_trivial121)
          hence "IncidP B p" 
            by (metis calculation colH_permut_231 colH_trivial122 line_on_plane')
          hence "IncidP C p" 
            using ‹A ≠ B› ‹ColH A B C› ‹IncidP A p› line_on_plane' by blast
          hence "IncidLP m p" 
            by (metis betH_colH Is_line Is_plane ‹BetH E G A› ‹C ≠ E› ‹IncidL C m› 
                ‹IncidL E m› ‹IncidP A p› ‹IncidP G p› colH_permut_321 
                line_on_plane line_on_plane')
          moreover have "¬ IncidL A m" 
            by (simp add: ‹¬ IncidL A m›)
          moreover have "cut m G D" 
            by (simp add: ‹local.cut m G D›)
          ultimately show ?thesis 
            by blast
        qed
        ultimately have "cut m G A ∨ cut m D A" 
          by blast
        moreover
        {
          assume "cut m G A"
          hence ?thesis 
            using ‹¬ (local.cut m A G ∨ local.cut m B G)› cut_comm by blast
        }
        moreover
        {
          assume "cut m D A"
          then obtain I where "IncidL I m" and "BetH D I A" 
            using local.cut_def by blast
          have "ColH D I A" 
            using ‹BetH D I A› between_col by fastforce
          obtain l1 where "IsL l1" and "IncidL A l1" and "IncidL B l1" and "IncidL C l1" 
            using ColH_def ‹ColH A B C› by blast
          obtain l2 where "IsL l2" and "IncidL B l2" and "IncidL C l2" and "IncidL D l2" 
            using ColH_def ‹ColH B C D› by blast
          obtain l3 where "IsL l3" and "IncidL D l3" and "IncidL I l3" and "IncidL A l3" 
            using ColH_def ‹ColH D I A› by blast
          have "A ≠ D" 
            using ‹¬ ColH G D A› colH_trivial122 by blast
          hence "BetH D C A" 
            by (metis ‹BetH D I A› ‹C ≠ B› ‹IncidL A l1› ‹IncidL A l3› 
                ‹IncidL B l1› ‹IncidL B l2› ‹IncidL C l1› ‹IncidL C l2› ‹IncidL C m› 
                ‹IncidL D l2› ‹IncidL D l3› ‹IncidL I l3› ‹IncidL I m› ‹¬ IncidL A m› 
                inter_incid_uniquenessH)
          hence "BetH A C D" 
            using between_comm by blast
        }
        ultimately have ?thesis
          by blast
      }
      ultimately have ?thesis 
        by blast
    }
    moreover
    {
      assume "E = G"
      hence ?thesis 
        using ColH_def ‹BetH B G F› ‹ColH C E F› ‹E ≠ F› ‹¬ ColH F C B› 
          between_col inter_incid_uniquenessH by fastforce
    }
    moreover
    {
      assume "G = A"
      hence ?thesis 
        by (metis ‹A ≠ B› ‹BetH B G F› ‹ColH A B C› ‹¬ ColH F C B› 
            between_col inter_uniquenessH ncolH_distincts)
    }
    ultimately have ?thesis
      using Bet_def ‹Bet E G A› by blast
  }
  moreover
  {
    assume "B = G"
    hence ?thesis 
      using ColH_def ‹A ≠ B› ‹Bet E G A› ‹ColH A B C› ‹¬ ColH A C E› 
        bet_colH inter_incid_uniquenessH by fastforce
  }
  moreover
  {
    assume "G = F"
    hence False
      by (metis ‹Bet E G A› ‹ColH C E F› ‹E ≠ F› ‹G = F› ‹¬ ColH A C E› 
          bet_colH colH_permut_321 colH_trans colH_trivial122) 
    hence ?thesis
      by blast
  }
  ultimately show ?thesis 
    using Bet_def ‹Bet B G F› by blast
qed

lemma betH_trans2:
  assumes "BetH A B C" and 
    "BetH B C D"
  shows "BetH A B D" 
  using assms(1) assms(2) betH_trans1 between_comm by blast

lemma betH_trans: 
  assumes "BetH A B C" and
    "BetH B C D" 
  shows "BetH A B D ∧ BetH A C D" 
  using assms(1) assms(2) betH_trans1 betH_trans2 by blast

lemma not_cut3:
  assumes "IncidP A p" and
    "IncidP B p" and
    "IncidP C p" and
    "IncidLP l p" and
    "¬ IncidL A l" and
    "¬ ColH A B C" and
    "¬ cut l A B" and
    "¬ cut l A C" 
  shows "¬ cut l B C" 
  by (meson colH_permut_312 cut_comm IncidLP_def assms(1) assms(2) assms(3) 
      assms(4) assms(5) assms(6) assms(7) assms(8) pasch)

lemma betH_trans0:
  assumes "BetH A B C" and
    "BetH A C D" 
  shows "BetH B C D ∧ BetH A B D" 
proof -
  have "A ≠ B" 
    using assms(1) betH_distincts by auto
  have "A ≠ C" 
    using assms(1) between_diff by auto
  have "A ≠ D" 
    using assms(2) between_diff by presburger
  obtain G where "¬ ColH A B G" 
    using ‹A ≠ B› ncolH_exists by presburger
  have "B ≠ G" 
    using ‹¬ ColH A B G› colH_trivial122 by blast
  obtain F where "BetH B G F" 
    using ‹B ≠ G› between_out by blast
  have "B ≠ F" 
    using ‹BetH B G F› between_diff by auto
  {
    assume "C = F"
    have "ColH B F A" 
      using ‹C = F› assms(1) between_col colH_permut_231 by presburger
    moreover have "ColH B F B" 
      by (simp add: colH_trivial121)
    moreover have "ColH B F G" 
      using ‹BetH B G F› betH_expand colH_permut_132 by blast
    ultimately have "ColH A B G" 
      using colH_trans ‹B ≠ F› by blast
    hence ?thesis 
      by (simp add: ‹¬ ColH A B G›)
  }
  moreover
  {
    assume "C ≠ F"
    obtain l where "IncidL C l" and "IncidL F l" 
      using ‹C ≠ F› line_existence by blast
    {
      assume "cut l A B"
      then obtain X where "IncidL X l" and "BetH A X B" 
        using local.cut_def by blast
      hence "X = C"
      proof -
        have "¬ ColH A B F" 
          by (meson ColH_def ‹B ≠ F› ‹BetH B G F› ‹¬ ColH A B G› 
              between_col inter_incid_uniquenessH)
        moreover have "ColH A B X" 
          by (simp add: ‹BetH A X B› between_col colH_permut_132)
        moreover have "ColH A B C" 
          using assms(1) betH_colH by presburger
        moreover have "ColH F C X" 
          using ColH_def Is_line ‹IncidL C l› ‹IncidL F l› ‹IncidL X l› by blast
        moreover have "ColH F C C" 
          by (simp add: colH_trivial122)
        ultimately show ?thesis
          by (metis inter_uniquenessH)
      qed
      have False 
        using ‹BetH A X B› ‹X = C› assms(1) between_comm between_only_one by blast
    }
    hence "¬ cut l A B" 
      by blast
    {
      assume "cut l B G"
      obtain X where "IncidL X l" and "BetH B X G" 
        using ‹local.cut l B G› local.cut_def by blast
      hence "ColH B X F" 
        by (meson ‹BetH B G F› ‹B ≠ G› between_col colH_permut_132 
            colH_trans colH_trivial121)
      hence False 
        using ColH_def ‹BetH B G F› ‹BetH B X G› ‹IncidL F l› ‹IncidL X l› 
          ‹local.cut l B G› between_comm between_only_one inter_incid_uniquenessH 
          local.cut_def by blast
    }
    hence "¬ cut l B G" 
      by blast
    obtain p where "IncidP A p" and "IncidP B p" and "IncidP G p" 
      using ‹¬ ColH A B G› plan_existence by blast
    have "¬ cut l A G"
    proof -
      have "IncidLP l p" 
        by (metis Hilbert_neutral_dimensionless.line_on_plane' 
            Hilbert_neutral_dimensionless_axioms Is_line Is_plane ‹BetH B G F› ‹C ≠ F›
            ‹IncidL C l› ‹IncidL F l› ‹IncidP A p› ‹IncidP B p› ‹IncidP G p› 
            assms(1) betH_expand line_on_plane)
      moreover
      {
        assume "IncidL B l"
        have "ColH B C G" 
          by (meson ColH_def ‹B ≠ F› ‹BetH B G F› ‹IncidL B l› ‹IncidL C l› 
              ‹IncidL F l› between_col inter_incid_uniquenessH)
        have "ColH B F C" 
          using ColH_def Is_line ‹IncidL B l› ‹IncidL C l› ‹IncidL F l› by blast
        hence False 
          using betH_expand colH_permut_231 colH_trans colH_trivial121 
            ‹ColH B C G› ‹¬ ColH A B G› assms(1) by fast
      }
      hence "¬ IncidL B l" 
        by blast
      moreover have "¬ ColH B A G" 
        using ‹¬ ColH A B G› colH_permut_213 by blast
      moreover have "¬ cut l B A" 
        using ‹¬ local.cut l A B› cut_comm by blast
      ultimately show ?thesis 
        using ‹IncidP A p› ‹IncidP B p› ‹IncidP G p› ‹¬ local.cut l B G› not_cut3 by blast
    qed 
    have "cut l A G ∨ cut l D G"
    proof -
      {
        assume "ColH A D G"
        have "ColH A C A" 
          by (simp add: colH_trivial121)
        moreover have "ColH A C D" 
          by (simp add: assms(2) between_col)
        moreover have "ColH A C B" 
          using assms(1) between_col colH_permut_132 by blast
        ultimately have "ColH A D B" 
          using ‹A ≠ C› colH_trans by blast
        hence False 
          using ‹A ≠ D› ‹ColH A D G› ‹¬ ColH A B G› colH_trans colH_trivial121 by blast
      }
      hence "¬ ColH A D G" 
        by blast
      then obtain p where "IncidP A p" and "IncidP D p" and "IncidP G p" 
        using plan_existence by blast
      show ?thesis
      proof -
        have "¬ ColH A D G" 
          by (simp add: ‹¬ ColH A D G›)
        moreover have "IsP p" 
          using Is_plane ‹IncidP D p› by fastforce
        moreover have "IsL l" 
          using Is_line ‹IncidL C l› by auto
        moreover have "IncidP A p" 
          by (simp add: ‹IncidP A p›)
        moreover have "IncidP D p" 
          by (simp add: ‹IncidP D p›)
        moreover have "IncidP G p" 
          using ‹IncidP G p› by auto
        moreover 
        have "IncidP C p" 
          by (metis ‹A ≠ D› assms(2) between_col calculation(4) calculation(5) 
              colH_permut_312 line_on_plane')
        have "IncidP F p" 
          by (meson ‹A ≠ C› ‹B ≠ G› ‹BetH B G F› ‹IncidP C p› assms(1) 
              between_col calculation(4) calculation(6) colH_permut_132 line_on_plane')
        hence "IncidLP l p" 
          using ‹C ≠ F› ‹IncidL C l› ‹IncidL F l› ‹IncidP C p› calculation(2) 
            calculation(3) line_on_plane by blast
        moreover 
        {
          assume "IncidL G l" 
          have "ColH G F C" 
            using ColH_def Is_line ‹IncidL C l› ‹IncidL F l› ‹IncidL G l› by blast
          hence "ColH B C G" 
            using ‹BetH B G F› betH_colH colH_permut_231 colH_trans colH_trivial121 by blast
          hence False 
            by (metis betH_expand colH_permut_231 colH_trans colH_trivial121
                ‹¬ ColH A B G› assms(1))
        }
        hence "¬ IncidL G l" 
          by blast
        moreover have "cut l A D"
        proof -
          {
            assume "IncidL A l"
            hence "ColH A C F" 
              using ColH_def Is_line ‹IncidL C l› ‹IncidL F l› by blast
            have "ColH A B F" 
              using ‹ColH A C F› assms(1) betH_colH colH_permut_132 colH_trans 
                colH_trivial121 by blast
            hence False 
              by (metis ‹B ≠ F› ‹BetH B G F› ‹¬ ColH A B G› between_col 
                  colH_permut_231 colH_trans colH_trivial121)
          }
          hence "¬ IncidL A l" 
            by blast
          moreover
          {
            assume "IncidL D l" 
            hence "ColH C D F" 
              using ColH_def ‹IncidL C l› ‹IncidL F l› ‹IsL l› by auto
            hence "ColH A C F" 
              using assms(2) betH_colH colH_permut_231 colH_trans colH_trivial121 by blast
            hence "ColH A B F" 
              by (metis assms(1) betH_colH colH_permut_312 colH_trans colH_trivial121)
            hence False 
              by (metis ‹B ≠ F› ‹BetH B G F› ‹¬ ColH A B G› between_col 
                  colH_permut_231 colH_trans colH_trivial121)
          }
          hence "¬ IncidL D l" 
            by blast
          moreover have "IncidL C l" 
            by (simp add: ‹IncidL C l›)
          moreover have "BetH A C D" 
            by (simp add: assms(2))
          ultimately show ?thesis 
            using ‹IsL l› local.cut_def by blast
        qed
        ultimately show ?thesis 
          using pasch by blast
      qed
    qed
    moreover
    {
      assume "cut l D G"
      {
        assume "ColH D G B"
        have "ColH A B D" 
          by (meson ‹A ≠ C› assms(1) assms(2) between_col colH_permut_132 
              colH_trans colH_trivial121)
        have "B ≠ D" 
          using ‹¬ local.cut l A G› ‹¬ local.cut l B G› calculation by auto
        hence "ColH A B G" 
          by (meson ColH_def ‹ColH A B D› ‹ColH D G B› inter_incid_uniquenessH)
        hence False 
          using ‹¬ ColH A B G› by blast
      }
      hence "¬ ColH D G B"
        by blast
      {
        assume "IncidL B l" 
        hence "ColH B F C" 
          using ColH_def Is_line ‹IncidL C l› ‹IncidL F l› by blast
        have "B ≠ C" 
          using assms(1) betH_distincts by presburger
        hence "ColH A B G" 
          by (metis ‹B ≠ F› ‹BetH B G F› ‹ColH B F C› assms(1) between_col 
              colH_permut_231 colH_trans colH_trivial121)
        hence False
          by (simp add: ‹¬ ColH A B G›)
      }
      hence "¬ IncidL B l" 
        by blast
      obtain p where "IncidP D p" and "IncidP G p" and "IncidP B p" 
        using ‹¬ ColH D G B› plan_existence by blast
      have "(¬ ColH D G B ∧ IncidP D p ∧ IncidP G p ∧ IncidP B p ∧ 
    IncidLP l p ∧ ¬ IncidL B l ∧ cut l D G) ⟶ (cut l D B ∨ cut l G B)" 
        using Is_line Is_plane ‹IncidL C l› pasch by blast
      moreover
      have "(¬ ColH D G B ∧ IncidP D p ∧ IncidP G p ∧ IncidP B p ∧ 
    IncidLP l p ∧ ¬ IncidL B l ∧ cut l D G)" 
      proof -
        have "¬ ColH D G B ∧ IncidP D p ∧ IncidP G p ∧ IncidP B p" 
          by (simp add: ‹IncidP B p› ‹IncidP D p› ‹IncidP G p› ‹¬ ColH D G B›)
        moreover have "IncidLP l p"
        proof -
          have "ColH B D C" 
            by (meson ‹A ≠ C› assms(1) assms(2) between_col colH_permut_132 
                colH_trans colH_trivial122)
          hence "IncidP C p" 
            by (metis calculation colH_trivial121 line_on_plane')
          moreover have "IncidP F p"     
            using ‹BetH B G F› ‹IncidP B p› ‹IncidP G p› betH_colH line_on_plane' by blast
          ultimately show ?thesis
            using Is_line Is_plane ‹C ≠ F› ‹IncidL C l› ‹IncidL F l› line_on_plane by blast
        qed
        moreover have "¬ IncidL B l"  
          by (simp add: ‹¬ IncidL B l›)
        moreover have "cut l D G"  
          by (simp add: ‹local.cut l D G›)
        ultimately show ?thesis 
          by blast
      qed
      ultimately have "cut l D B ∨ cut l G B" 
        using ‹¬ ColH D G B ∧ IncidP D p ∧ IncidP G p ∧ IncidP B p ∧ 
      IncidLP l p ∧ ¬ IncidL B l ∧ local.cut l D G ⟶ local.cut l D B ∨ local.cut l G B› 
        by blast
      moreover
      {
        assume "cut l D B"
        then obtain C' where "IncidL C' l" and "BetH D C' B" 
          using local.cut_def by blast
        have "ColH C C' F" 
          using ColH_def Is_line ‹IncidL C l› ‹IncidL C' l› ‹IncidL F l› by blast
        have "¬ ColH A B F" 
          by (metis ‹BetH B G F› ‹¬ ColH A B G› betH_colH colH_permut_312 
              colH_trans colH_trivial122)
        have "ColH B D A" 
          by (metis (full_types) ‹A ≠ C› assms(1) assms(2) between_col colH_trans 
              ncolH_distincts)
        hence "ColH A B C'" 
          using ColH_def ‹BetH D C' B› betH_colH inter_incid_uniquenessH by fastforce
        then have "C = C'" using inter_uniquenessH 
          by (metis (full_types) ‹ColH C C' F› ‹¬ ColH A B F› assms(1) 
              betH_colH ncolH_distincts)
        hence "BetH B C D ∧ BetH A B D"  
          using ‹BetH D C' B› assms(1) betH_trans between_comm by blast
      }
      moreover
      {
        assume "cut l G B"
        hence "BetH B C D ∧ BetH A B D"  
          using ‹¬ local.cut l B G› cut_comm by blast
      }
      ultimately have "BetH B C D ∧ BetH A B D"  
        by blast
    }
    ultimately have "BetH B C D ∧ BetH A B D" 
      using ‹¬ local.cut l A G› by fastforce
  }
  ultimately show ?thesis 
    by blast
qed 

lemma betH_outH2__betH:
  assumes "BetH A B C" and
    "outH B C C'" and
    "outH B A A'"
  shows "BetH A' B C'" 
proof -

  have "BetH B C C' ∨ BetH B C' C ∨ (B ≠ C ∧ C = C')" 
    using assms(2) outH_def by blast
  moreover have "BetH B A A' ∨ BetH B A' A ∨ (B ≠ A ∧ A = A')" 
    using assms(3) outH_def by blast
  moreover
  {
    assume "BetH B C C'" 
    hence "BetH A' B C" 
      using assms(1) betH_trans betH_trans0 between_comm calculation(2) by blast
  }
  moreover
  {
    assume "BetH B C' C" 
    hence "BetH A' B C" 
      using assms(1) betH_trans betH_trans0 between_comm calculation(2) by blast
  }
  moreover
  {
    assume "B ≠ C ∧ C = C'" 
    hence "BetH A' B C" 
      using assms(1) betH_trans betH_trans0 between_comm calculation(2) by blast
  }
  ultimately show ?thesis
    by (meson betH_trans betH_trans0 between_comm)
qed

lemma cong_existence':
  fixes A B::'p
  assumes "A ≠ B" and
    "IncidL M l" 
  shows "∃ A' B'. IncidL A' l ∧ IncidL B' l ∧ BetH A' M B' ∧ CongH M A' A B ∧ CongH M B' A B" 
proof -
  have "∃ P. IncidL P l ∧ M ≠ P" 
    by (metis Is_line assms(2) two_points_on_line)
  then obtain P where "IncidL P l" and "M ≠ P" 
    by blast
  obtain P' where "BetH P M P'" 
    using ‹M ≠ P› between_out by presburger
  obtain A' where "IncidL A' l" and "outH M P A'" and "CongH M A' A B" 
    using Is_line ‹IncidL P l› ‹M ≠ P› assms(1) assms(2) cong_existence by blast
  moreover
  have "IncidL P' l" 
    using ColH_def ‹BetH P M P'› ‹IncidL P l› assms(2) betH_colH inter_incid_uniquenessH by blast
  then obtain B' where "IncidL B' l" and "outH M P' B'" and "CongH M B' A B" 
    by (metis Is_line ‹BetH P M P'› assms(1) assms(2) betH_distincts cong_existence)
  ultimately show ?thesis 
    using ‹BetH P M P'› betH_outH2__betH by blast
qed

lemma betH_to_bet:
  assumes "BetH A B C" 
  shows "Bet A B C ∧ A ≠ B ∧ B ≠ C ∧ A ≠ C" 
  using Bet_def assms betH_distincts by presburger

lemma betH_line:
  assumes "BetH A B C" 
  shows "∃ l. IncidL A l ∧ IncidL B l ∧ IncidL C l" 
  by (meson ColH_def assms betH_colH)

(****************** between_identity ************************)

lemma bet_identity: 
  assumes "Bet A B A"
  shows "A = B" 
  using Bet_def assms between_diff by blast

(************************************************************)

lemma morph: 
  assumes "IsL l" and
    "IsL m " and
    "EqL l m"
  shows "∀ A. IncidL A l ⟷ IncidL A m" 
  using EqL_sym IncidL_morphism assms(1) assms(2) assms(3) by blast

lemma point3_online_exists:
  assumes "IncidL A l" and 
    "IncidL B l"
  shows "∃ C. IncidL C l  ∧ C ≠ A ∧ C ≠ B" 
  by (metis (full_types) assms(2) betH_distincts cong_existence' lower_dim_2)

lemma not_betH121:
  shows "¬ BetH A B A" 
  using between_diff by blast

(***************************** cong_identity ***********************)

lemma cong_identity:
  assumes "Cong A B C C"
  shows "A = B" 
  using Cong_def assms by presburger

(************************ cong_inner_transitivity ****************************)

lemma cong_inner_transitivity:
  assumes "Cong A B C D" and
    "Cong A B E F"
  shows "Cong C D E F" 
  by (metis Cong_def assms(1) assms(2) cong_pseudo_transitivity)

lemma other_point_on_line:
  assumes "IncidL A l"
  shows "∃ B. A ≠ B ∧ IncidL B l" 
  by (metis Is_line assms two_points_on_line)

lemma bet_disjoint:
  assumes "BetH A B C"
  shows "disjoint A B B C" 
proof -
  {
    assume "¬ disjoint A B B C"
    then obtain P where "BetH A P B" and "BetH B P C" 
      using disjoint_def by blast
    have "BetH P B C ∧ BetH A P C" 
      using betH_trans0 ‹BetH A P B› assms by blast
    hence False 
      using ‹BetH B P C› between_only_one' by blast
  }
  thus ?thesis 
    by blast
qed

lemma addition_betH:
  assumes "BetH A B C" and
    "BetH A' B' C'" and
    "CongH A B A' B'" and
    "CongH B C B' C'"
  shows "CongH A C A' C'" 
  using addition assms(1) assms(2) assms(3) assms(4) bet_disjoint between_col by blast

lemma outH_trivial: 
  assumes "A ≠ B" 
  shows "outH A B B" 
  by (simp add: assms outH_def)

lemma same_side_refl:
  assumes "IsL l" and (** ROLL ADD IsL l **)
    "¬ IncidL A l" 
  shows "same_side A A l"
proof -
  obtain x x0 where "IncidL x0 l" and "IncidL x l" and "x ≠ x0" 
    using two_points_on_line assms(1) by blast
  {
    assume "A = x" 
    hence "same_side A A l" 
      using ‹IncidL x l› assms(2) by fastforce
  }
  moreover
  {
    assume "A ≠ x" 
    obtain x1 where "BetH A x x1" 
      by (metis ‹IncidL x l› assms(2) between_out)
    have "¬ IncidL x1 l" 
      using ‹BetH A x x1› ‹IncidL x l› assms(2) betH_expand betH_line 
        inter_incid_uniquenessH by blast
    moreover have "∃ I. IncidL I l ∧ BetH A I x1" 
      using ‹BetH A x x1› ‹IncidL x l› by blast
    ultimately have "same_side A A l" 
      using assms(1) assms(2) local.cut_def same_side_def by blast
  }
  ultimately show ?thesis 
    by blast
qed

lemma same_side_prime_refl: 
  assumes "¬ ColH A B C"
  shows "same_side' C C A B" 
  using ColH_def assms ncolH_distincts same_side'_def same_side_refl by presburger

lemma outH_expand: 
  assumes "outH A B C" 
  shows "outH A B C ∧ ColH A B C ∧ A ≠ C ∧ A ≠ B" 
  by (metis assms betH_colH colH_permut_132 colH_trivial122 outH_def)

lemma construction_uniqueness:
  assumes "BetH A B D" and
    "BetH A B E" and
    "CongH B D B E"
  shows "D = E" 
proof -
  have "A ≠ D" 
    using assms(1) between_diff by blast
  have "A ≠ E" 
    using assms(2) not_betH121 by blast
  have "ColH A B D" 
    by (simp add: assms(1) betH_colH)
  have "ColH A B E" 
    using assms(2) betH_colH by fastforce
  have "A ≠ B" 
    using assms(1) betH_distincts by auto
  then obtain C where "¬ ColH A B C" 
    using  ncolH_exists by presburger
  have "CongaH A C D A C E"
  proof -
    have"¬ ColH A C D" 
      by (meson ‹A ≠ D› ‹ColH A B D› ‹¬ ColH A B C› colH_permut_132
          colH_trans colH_trivial121)
    moreover have "¬ ColH A C E" 
      by (metis ‹A ≠ E› ‹ColH A B E› ‹¬ ColH A B C› colH_trivial121 
          colH_trivial122 inter_uniquenessH)
    moreover have "CongH A C A C" 
      by (metis calculation(1) colH_trivial112 congH_refl)
    moreover have "CongH A D A E" 
      by (metis addition_betH assms(1) assms(2) assms(3) congH_refl)
    moreover have "CongaH C A D C A E"  
    proof-
      have "CongaH C A B C A B" 
        by (meson ‹¬ ColH A B C› colH_permut_231 conga_refl)
      moreover have "outH A C C" 
        using ‹¬ ColH A C D› ncolH_distincts outH_trivial by presburger
      moreover have "outH A B D" 
        by (simp add: assms(1) outH_def)
      moreover have "outH A B E" 
        by (simp add: assms(2) outH_def)
      ultimately show ?thesis 
        using conga_out_conga by blast
    qed
    ultimately show ?thesis 
      using cong_5 by blast
  qed
  moreover have "¬ ColH D C A" 
    by (metis ncolH_distincts ‹A ≠ D› ‹ColH A B D› ‹¬ ColH A B C› inter_uniquenessH)
  moreover hence "¬ ColH A C D" 
    using colH_permut_321 by blast
  moreover hence "¬ ColH C A D" 
    using colH_permut_213 by blast
  moreover have "same_side' D E C A" 
  proof -
    obtain F where "BetH B A F" 
      using ‹A ≠ B› between_out by fastforce
    obtain l where "IncidL C l" and "IncidL A l" 
      using ColH_def colH_trivial122 by blast
    have "C ≠ A" 
      using calculation(2) colH_trivial122 by auto
    moreover
    have "∀ l. IsL l ∧ IncidL C l ∧ IncidL A l ⟶ same_side D E l"
    proof -
      {
        fix l
        assume "IsL l" and "IncidL C l" and "IncidL A l"
        have "cut l D F" 
        proof -
          {
            assume "IncidL D l" 
            have "ColH A C D" 
              using ColH_def ‹IncidL A l› ‹IncidL C l› ‹IncidL D l› ‹IsL l› by blast
            have False 
              using ‹ColH A C D› ‹¬ ColH A C D› by auto
          }
          hence "¬ IncidL D l" 
            by blast
          moreover
          {
            assume "IncidL F l" 
            have "ColH A C F" 
              using ColH_def Is_line ‹IncidL A l› ‹IncidL C l› ‹IncidL F l› by blast
            have False 
              using ColH_def ‹BetH B A F› ‹IncidL A l› ‹IncidL C l› ‹IncidL F l›
                ‹IsL l› ‹¬ ColH A B C› betH_distincts betH_line inter_incid_uniquenessH by blast
          }
          hence "¬ IncidL F l" 
            by blast
          moreover have "∃ I. IncidL I l ∧ BetH D I F" 
            using ‹BetH B A F› ‹IncidL A l› assms(1) betH_trans between_comm by blast
          ultimately show ?thesis
            by (simp add: ‹IsL l› local.cut_def)
        qed
        moreover have "cut l E F" 
        proof -
          {
            assume "IncidL E l" 
            have "ColH A C E" 
              using ColH_def ‹IncidL A l› ‹IncidL C l› ‹IncidL E l› ‹IsL l› by blast
            hence False 
              using ColH_def ‹A ≠ E› ‹¬ ColH A B C› assms(2) betH_line 
                inter_incid_uniquenessH by blast
          }
          hence "¬ IncidL E l" 
            by blast
          moreover
          {
            assume "IncidL F l" 
            have "ColH A C F" 
              using ‹IncidL F l› ‹local.cut l D F› local.cut_def by auto
            hence False 
              using ‹IncidL F l› ‹local.cut l D F› local.cut_def by blast
          }
          hence "¬ IncidL F l" 
            by blast
          moreover have "∃ I. IncidL I l ∧ BetH E I F" 
            using ‹BetH B A F› ‹IncidL A l› assms(2) betH_trans between_comm by blast
          ultimately show ?thesis
            by (simp add: ‹IsL l› local.cut_def)
        qed
        ultimately have "same_side D E l"
          using ‹IsL l› same_side_def by blast
      }
      thus ?thesis 
        by blast
    qed
    ultimately show ?thesis 
      using same_side'_def by auto
  qed
  ultimately have "outH C D E" 
    using same_side_prime_refl by (meson cong_4_uniqueness conga_refl)
  thus ?thesis 
    using ‹ColH A B D› ‹ColH A B E› ‹¬ ColH A B C› colH_trivial122 
      inter_uniquenessH outH_expand by blast
qed

lemma out_distinct:
  assumes "outH A B C" 
  shows "A ≠ B ∧ A ≠ C" 
  using assms outH_expand by auto

lemma out_same_side:
  assumes "IncidL A l" and
    "¬ IncidL B l" and
    "outH A B C"
  shows "same_side B C l" 
proof -
  have "A ≠ B" 
    using assms(1) assms(2) by blast
  obtain P where "BetH B A P" 
    using ‹A ≠ B› between_out by presburger
  {
    assume "IncidL P l"
    have "ColH B A P" 
      by (simp add: ‹BetH B A P› between_col)
    obtain ll where "IncidL B ll" and "IncidL A ll" and "IncidL P ll" 
      using ‹BetH B A P› betH_line by blast
    hence "EqL l ll" 
      by (metis Is_line ‹BetH B A P› ‹IncidL P l› assms(1) betH_distincts line_uniqueness)
    hence False 
      using Is_line ‹IncidL B ll› ‹IncidL P l› assms(2) morph by blast
  }
  hence "¬ IncidL P l"
    by blast
  have "cut l B P" 
    using assms(1) ‹BetH B A P› Is_line ‹¬ IncidL P l› assms(2) local.cut_def by blast
  moreover have "cut l C P"
  proof -
    have "¬ IncidL C l"
      using ColH_def assms(1) assms(2) assms(3) inter_incid_uniquenessH 
        outH_expand by blast
    moreover have "BetH C A P" 
      by (metis betH_outH2__betH betH_to_bet outH_trivial ‹BetH B A P› assms(3))
    ultimately show ?thesis 
      using assms(1) Is_line ‹¬ IncidL P l› local.cut_def by blast
  qed
  ultimately show ?thesis
    using Is_line assms(1) same_side_def by blast
qed

lemma between_one:
  assumes "A ≠ B" and
    "A ≠ C" and
    "B ≠ C" and
    "ColH A B C" 
  shows "BetH A B C ∨ BetH B C A ∨ BetH B A C" 
proof -
  obtain D where "¬ ColH A C D" 
    using assms(2) ncolH_exists by presburger
  have "B ≠ D" 
    using ‹¬ ColH A C D› assms(4) colH_permut_132 by blast
  obtain G where "BetH B D G" 
    using ‹B ≠ D› between_out by blast
  have "A ≠ D" 
    using ‹¬ ColH A C D› colH_trivial121 by force
  then obtain lAD where "IsL lAD" and "IncidL A lAD" and "IncidL D lAD" 
    using line_existence by blast
  have "C ≠ D" 
    using ‹¬ ColH A C D› colH_trivial122 by blast
  then obtain lCD where "IsL lCD" and "IncidL C lCD" and "IncidL D lCD" 
    using line_existence by blast
  {
    assume "ColH B G C"
    hence False 
      by (metis ‹BetH B D G› ‹¬ ColH A C D› assms(3) assms(4) between_col 
          colH_permut_312 colH_trans colH_trivial122 not_betH121)
  }
  hence "¬ ColH B G C" 
    by blast
  {
    assume "ColH B G A"
    hence False 
      by (meson colH_permut_312 colH_trans colH_trivial122 ‹¬ ColH B G C› 
          assms(1) assms(4))
  }
  hence "¬ ColH B G A" 
    by blast
  have "¬ IncidL C lAD" 
    using ColH_def ‹IncidL A lAD› ‹IncidL D lAD› ‹IsL lAD› ‹¬ ColH A C D› by blast
  have "¬ IncidL A lCD" 
    using ‹A ≠ D› ‹IncidL A lAD› ‹IncidL C lCD› ‹IncidL D lAD› ‹IncidL D lCD› 
      ‹¬ IncidL C lAD› inter_incid_uniquenessH by blast
  {
    assume "IncidL B lAD"
    have "ColH A B D" 
      using ColH_def ‹IncidL A lAD› ‹IncidL B lAD› ‹IncidL D lAD› ‹IsL lAD› by blast
    hence False 
      using ‹¬ ColH A C D› assms(1) assms(4) colH_trans colH_trivial121 by blast
  }
  hence "¬ IncidL B lAD" 
    by blast
  {
    assume "IncidL G lAD"
    have "ColH A D G" 
      using ColH_def Is_line ‹IncidL A lAD› ‹IncidL D lAD› ‹IncidL G lAD› by blast
    hence False 
      using betH_colH ‹BetH B D G› ‹IncidL D lAD› ‹IncidL G lAD› ‹¬ IncidL B lAD›
        betH_line inter_incid_uniquenessH by blast
  }
  hence "¬ IncidL G lAD" 
    by blast
  have "cut lAD B G" 
    using ‹BetH B D G› ‹IncidL D lAD› ‹IsL lAD› ‹¬ IncidL B lAD› ‹¬ IncidL G lAD›
      local.cut_def by blast
  {
    assume "IncidL B lCD"
    have "ColH B C D" 
      using ColH_def ‹IncidL B lCD› ‹IncidL C lCD› ‹IncidL D lCD› ‹IsL lCD› by blast
    hence False 
      by (meson colH_permut_231 colH_trans colH_trivial122 ‹¬ ColH A C D› assms(3) assms(4))
  }
  hence "¬ IncidL B lCD" 
    by blast
  {
    assume "IncidL G lCD"
    have "ColH C D G" 
      using ColH_def ‹IncidL C lCD› ‹IncidL D lCD› ‹IncidL G lCD› ‹IsL lCD› by blast
    hence False 
      using betH_colH ‹BetH B D G› ‹IncidL D lCD› ‹IncidL G lCD› ‹¬ IncidL B lCD›
        betH_line inter_incid_uniquenessH by blast
  }
  hence "¬ IncidL G lCD" 
    by blast
  have "cut lCD B G" 
    using Is_line ‹BetH B D G› ‹IncidL D lCD› ‹¬ IncidL B lCD› 
      ‹¬ IncidL G lCD› local.cut_def by blast
  obtain bgc where "IsP bgc" and "IncidP B bgc" and "IncidP G bgc" and "IncidP C bgc" 
    using ‹¬ ColH B G C› plan_existence by blast
  obtain bga where "IsP bga" and "IncidP B bga" and "IncidP G bga" and "IncidP A bga" 
    using ‹¬ ColH B G A› plan_existence by blast
  have "IncidLP lAD bgc"
    using line_on_plane
    by (metis ‹A ≠ D› ‹BetH B D G› ‹IncidL A lAD› ‹IncidL D lAD› ‹IncidP B bgc› ‹IncidP C bgc›
        ‹IncidP G bgc› ‹IsL lAD› ‹IsP bgc› ‹¬ ColH B G C› assms(4) between_col colH_permut_132
        colH_permut_321 line_on_plane' same_side'_def same_side_prime_refl) 
  have "IncidLP lCD bga" 
    using line_on_plane
    by (smt (verit, best) IncidLP_def IncidP_morphism ‹C ≠ D› ‹IncidL A lAD› ‹IncidL C lCD›
        ‹IncidL D lAD› ‹IncidL D lCD› ‹IncidLP lAD bgc› ‹IncidP A bga› ‹IncidP B bga› 
        ‹IncidP B bgc› ‹IncidP G bga› ‹IncidP G bgc› ‹IsL lCD› ‹IsP bga› ‹¬ ColH B G A› 
        assms(1,4) line_on_plane' plane_uniqueness) 
  show ?thesis
  proof -
    {
      assume "cut lAD B C"
      then obtain I where "IncidL I lAD" and "BetH B I C" 
        using local.cut_def by blast
      have "BetH A B C ∨ BetH B C A ∨ BetH B A C" 
      proof -
        {
          assume "cut lCD B A"
          {
            assume "A = I"
            have "BetH A B C ∨ BetH B C A ∨ BetH B A C" 
              by (simp add: ‹A = I› ‹BetH B I C›)
          }
          moreover
          {
            assume "A ≠ I"
            have "ColH A D I" 
              using ColH_def Is_line ‹IncidL A lAD› ‹IncidL D lAD› ‹IncidL I lAD› by blast
            have "¬ ColH B C D" 
              by (meson ‹¬ ColH A C D› assms(3) assms(4) colH_permut_231 
                  colH_trans colH_trivial122)
            have "ColH B C I" 
              by (simp add: ‹BetH B I C› betH_colH colH_permut_132)
            have "ColH B C A" 
              by (simp add: assms(4) colH_permut_231)
            have "ColH D A I" 
              using ‹ColH A D I› colH_permut_213 by blast
            have "ColH D A A" 
              by (simp add: colH_trivial122)
            hence False using inter_uniquenessH 
              by (metis ‹A ≠ I› ‹ColH B C A› ‹ColH B C I› ‹ColH D A I› ‹¬ ColH B C D›)
            hence "BetH A B C ∨ BetH B C A ∨ BetH B A C" 
              by blast
          }
          ultimately
          have "BetH A B C ∨ BetH B C A ∨ BetH B A C" 
            by fastforce
        }
        moreover 
        {
          assume "cut lCD G A"
          {
            assume "A = I"
            have "BetH A B C ∨ BetH B C A ∨ BetH B A C" 
              by (simp add: ‹A = I› ‹BetH B I C›)
          }
          moreover
          {
            assume "A ≠ I"
            have "ColH A D I" 
              using ColH_def Is_line ‹IncidL A lAD› ‹IncidL D lAD› ‹IncidL I lAD› by blast
            have "D ≠ A" 
              using ‹A ≠ D› by blast
            moreover have "¬ ColH B C D" 
              by (meson ‹¬ ColH A C D› assms(3) assms(4) colH_permut_231 
                  colH_trans colH_trivial122)
            moreover have "ColH B C I" 
              by (simp add: ‹BetH B I C› betH_colH colH_permut_132)
            moreover have "ColH B C A" 
              by (simp add: assms(4) colH_permut_231)
            moreover have "ColH D A I" 
              using ‹ColH A D I› colH_permut_213 by blast
            moreover have "ColH D A A" 
              by (simp add: colH_trivial122)
            hence False 
              by (metis ‹A ≠ I› calculation(2) calculation(3) calculation(4) 
                  calculation(5) inter_uniquenessH)
            hence "BetH A B C ∨ BetH B C A ∨ BetH B A C" 
              by blast
          }
          ultimately have "BetH A B C ∨ BetH B C A ∨ BetH B A C" 
            by blast
        }
        ultimately show ?thesis
          using ‹IncidLP lCD bga› ‹IncidP A bga› ‹IncidP B bga› ‹IncidP G bga›
            ‹IsL lCD› ‹IsP bga› ‹¬ ColH B G A› ‹¬ IncidL A lCD› 
            ‹local.cut lCD B G› pasch by blast
      qed
    }
    moreover 
    {
      assume "cut lAD G C"
      have "BetH A B C ∨ BetH B C A ∨ BetH B A C" 
      proof -
        {
          assume "cut lCD B A" 
          then obtain I where "IncidL I lCD" and "BetH B I A" 
            using local.cut_def by blast
          {
            assume "C = I"
            hence "BetH A B C ∨ BetH B C A ∨ BetH B A C" 
              by (simp add: ‹BetH B I A›)
          }
          moreover
          {
            assume "C ≠ I"
            have "ColH C D I" 
              using ColH_def Is_line ‹IncidL C lCD› ‹IncidL D lCD› ‹IncidL I lCD› by blast
            have "D ≠ C" 
              using ‹C ≠ D› by blast
            moreover have "¬ ColH A B D" 
              using ‹¬ ColH A C D› assms(1) assms(4) colH_trans colH_trivial121 by blast
            moreover have "ColH A B I" 
              by (simp add: ‹BetH B I A› betH_colH colH_permut_312)
            moreover have "ColH A B C" 
              by (simp add: assms(4))
            moreover have "ColH D C I" 
              by (simp add: ‹ColH C D I› colH_permut_213)
            moreover have "ColH D C C" 
              by (simp add: colH_trivial122)
            ultimately have False 
              using ‹C ≠ I› inter_uniquenessH by blast
            hence "BetH A B C ∨ BetH B C A ∨ BetH B A C" 
              by blast
          }
          ultimately have "BetH A B C ∨ BetH B C A ∨ BetH B A C" 
            by blast
        }
        moreover {
          assume"cut lCD G A" 
          obtain E where "IncidL E lAD" and "BetH G E C" 
            using local.cut_def ‹local.cut lAD G C› by blast
          obtain F where "IncidL F lCD" and "BetH G F A" 
            using ‹local.cut lCD G A› local.cut_def by blast
          {
            assume "ColH A G E"
            hence "ColH A C D" 
              using ‹BetH G E C› ‹¬ ColH B G A› assms(4) betH_colH 
                colH_permut_231 colH_trivial121 inter_uniquenessH by blast
            hence False 
              using ‹¬ ColH A C D› by auto
          }
          hence "¬ ColH A G E" 
            by blast
          have "C ≠ F" 
            using between_col ‹BetH G E C› ‹BetH G F A› ‹¬ ColH A G E›
              betH_trans0 colH_permut_312 by blast
          obtain lCF where "IsL lCF" and "IncidL C lCF" and "IncidL F lCF" 
            using ‹IncidL C lCD› ‹IncidL F lCD› ‹IsL lCD› by blast
          {
            assume "IncidL E lCF" 
            hence False
              by (metis (full_types) Hilbert_neutral_dimensionless.betH_expand
                  Hilbert_neutral_dimensionless_axioms ‹BetH G E C› ‹C ≠ F› ‹IncidL C lCD›
                  ‹IncidL C lCF› ‹IncidL E lCF› ‹IncidL F lCD› ‹IncidL F lCF›
                  ‹¬ IncidL G lCD› betH_line inter_incid_uniquenessH)
          }
          hence "¬ IncidL E lCF" 
            by blast
          have "cut lCF A G" 
            by (metis IncidL_morphism Is_line ‹BetH G F A› ‹C ≠ F› ‹IncidL C lCD› 
                ‹IncidL C lCF› ‹IncidL F lCD› ‹IncidL F lCF› ‹¬ IncidL A lCD›
                ‹¬ IncidL G lCD› between_comm line_uniqueness local.cut_def)
          obtain p where "IncidP A p" and "IncidP G p" and "IncidP E p" 
            using IncidLP_def ‹IncidL A lAD› ‹IncidL E lAD› ‹IncidLP lAD bgc›
              ‹IncidP G bgc› by blast
          have "IncidP C p" 
            using ‹BetH G E C› ‹IncidP E p› ‹IncidP G p› betH_colH line_on_plane' by blast
          moreover have "IncidP F p" 
            by (metis ‹BetH G F A› ‹IncidP A p› ‹IncidP G p› betH_colH 
                colH_permut_312 line_on_plane') 
          ultimately have "IncidLP lCF p" 
            using Is_plane ‹C ≠ F› ‹IncidL C lCF› ‹IncidL F lCF› ‹IsL lCF› 
              line_on_plane by blast
          { 
            assume "cut lCF A E"
            then obtain I where "IncidL I lCF" and "BetH A I E" 
              using local.cut_def by blast
            have "I = D" 
              by (metis (full_types) Hilbert_neutral_dimensionless.betH_colH 
                  Hilbert_neutral_dimensionless_axioms ‹BetH A I E› ‹C ≠ F› ‹IncidL A lAD› 
                  ‹IncidL C lCD› ‹IncidL C lCF› ‹IncidL D lAD› ‹IncidL D lCD› ‹IncidL E lAD› 
                  ‹IncidL F lCD› ‹IncidL F lCF› ‹IncidL I lCF› ‹¬ IncidL A lCD› 
                  betH_line inter_incid_uniquenessH)
            {
              assume "ColH A E C"
              have "A ≠ E" 
                using ‹BetH A I E› not_betH121 by fastforce
              have "ColH A D E" 
                using ‹BetH A I E› ‹I = D› between_col by auto
              hence "ColH A C D" 
                by (meson Hilbert_neutral_dimensionless.colH_permut_132 
                    colH_trans colH_trivial121 Hilbert_neutral_dimensionless_axioms
                    ‹A ≠ E› ‹ColH A E C›) 
              hence False 
                using ‹¬ ColH A C D› by blast
            }
            hence "¬ ColH A E C"
              by blast
            obtain lBD where "IncidL B lBD" and "IncidL D lBD" 
              using ‹B ≠ D› line_existence by blast
            have "cut lBD A E" 
              by (metis betH_colH cut_def 
                  Is_line ‹BetH A I E› ‹I = D› ‹IncidL A lAD› ‹IncidL B lBD› ‹IncidL D lAD› 
                  ‹IncidL D lBD› ‹IncidL E lAD› ‹¬ IncidL B lAD› inter_incid_uniquenessH)
            have "IncidLP lBD p" 
              by (metis IncidLP_def Is_line ‹B ≠ D› ‹I = D› ‹IncidL B lBD› ‹IncidL D lBD› 
                  ‹IncidL I lCF› ‹IncidLP lCF p› ‹IncidP A p› ‹IncidP C p› assms(2) assms(4) 
                  colH_permut_312 line_on_plane line_on_plane')
            { 
              assume "cut lBD A C"
              then obtain I where "IncidL I lBD" and "BetH A I C" 
                using local.cut_def by blast
              hence "ColH A I C" 
                using betH_colH by blast
              hence "I = B"
              proof -
                have "D ≠ B" 
                  using ‹B ≠ D› by auto
                moreover have "¬ ColH A C D" 
                  by (simp add: ‹¬ ColH A C D›)
                moreover have "ColH A C I" 
                  using ‹ColH A I C› colH_permut_132 by blast
                moreover have "ColH A C B" 
                  by (simp add: assms(4) colH_permut_132)
                moreover have "ColH D B I" 
                  using ColH_def Is_line ‹IncidL B lBD› ‹IncidL D lBD› ‹IncidL I lBD› by blast
                moreover have "ColH D B B" 
                  by (simp add: colH_trivial122)
                ultimately show ?thesis
                  using inter_uniquenessH by blast
              qed
              hence "BetH A B C ∨ BetH B C A ∨ BetH B A C" 
                using ‹BetH A I C› by auto
            }
            moreover {
              assume "cut lBD E C"
              then obtain I where "IncidL I lBD" and "BetH E I C" 
                using local.cut_def by blast
              hence "ColH E I C" 
                by (simp add: betH_colH)
              hence "I = G"
              proof -
                have "C ≠ E" 
                  using ‹IncidL E lAD› ‹¬ IncidL C lAD› by auto
                moreover have "¬ ColH D B C" 
                  by (metis ‹BetH B D G› ‹¬ ColH B G C› betH_colH colH_permut_213 
                      colH_trans colH_trivial122)
                moreover have "ColH D B I" 
                  using ColH_def Is_line ‹IncidL B lBD› ‹IncidL D lBD› ‹IncidL I lBD› by blast
                moreover have "ColH D B G" 
                  using ‹BetH B D G› between_col colH_permut_213 by blast
                moreover have "ColH C E I" 
                  using ‹ColH E I C› colH_permut_312 by blast
                moreover have "ColH C E G" 
                  by (simp add: ‹BetH G E C› between_col between_comm)
                ultimately show ?thesis
                  using inter_uniquenessH by blast
              qed
              hence "BetH A B C ∨ BetH B C A ∨ BetH B A C" 
                using ‹BetH E I C› ‹BetH G E C› between_only_one' by blast
            }
            ultimately have "BetH A B C ∨ BetH B C A ∨ BetH B A C"
              using pasch inter_incid_uniquenessH Is_line Is_plane ‹C ≠ D› ‹IncidL B lBD› 
                ‹IncidL C lCD› ‹IncidL D lBD› ‹IncidL D lCD› ‹IncidLP lBD p› ‹IncidP A p› 
                ‹IncidP C p› ‹IncidP E p› ‹¬ ColH A E C› ‹¬ IncidL B lCD›
                ‹local.cut lBD A E› by fastforce
          }
          moreover 
          {
            assume "cut lCF G E"
            then obtain I where "IncidL I lCF" and "BetH G I E" 
              using local.cut_def by blast
            hence "ColH G I E" 
              using betH_expand by blast
            have "I = C" 
            proof -
              have "F ≠ C" 
                using ‹C ≠ F› by auto
              moreover have "¬ ColH G E F" 
                using ‹BetH G F A› ‹¬ ColH A G E› betH_colH colH_permut_132
                  colH_trans colH_trivial121 by blast
              moreover have "ColH G E I" 
                using ‹ColH G I E› colH_permut_132 by presburger
              moreover have "ColH G E C" 
                by (simp add: ‹BetH G E C› betH_colH)
              moreover have "ColH F C I" 
                using ColH_def Is_line ‹IncidL C lCF› ‹IncidL F lCF› 
                  ‹IncidL I lCF› by blast
              moreover have "ColH F C C" 
                by (simp add: colH_trivial122)
              ultimately show ?thesis 
                using inter_uniquenessH by blast
            qed
            hence "BetH A B C ∨ BetH B C A ∨ BetH B A C" 
              using ‹BetH G E C› ‹BetH G I E› between_comm between_only_one by blast
          }
          ultimately have "BetH A B C ∨ BetH B C A ∨ BetH B A C" 
            using Is_plane ‹IncidLP lCF p› ‹IncidP A p› ‹IncidP E p› ‹IncidP G p› 
              ‹IsL lCF› ‹¬ ColH A G E› ‹¬ IncidL E lCF› ‹local.cut lCF A G› 
              pasch by blast
        }
        ultimately show ?thesis 
          using ‹IncidLP lCD bga› ‹IncidP A bga› ‹IncidP B bga› ‹IncidP G bga›
            ‹IsL lCD› ‹IsP bga› ‹¬ ColH B G A› ‹¬ IncidL A lCD› 
            ‹local.cut lCD B G› pasch by blast
      qed
    }
    ultimately show ?thesis 
      using pasch ‹IsL lAD› ‹IsP bgc› ‹IncidLP lAD bgc› ‹IncidP B bgc› ‹IncidP C bgc›
        ‹IncidP G bgc› ‹¬ ColH B G C› ‹¬ IncidL C lAD› ‹local.cut lAD B G› by blast
  qed
qed

lemma betH_dec: 
  (*assumes "A ≠ B" and
"B ≠ C" and
"A ≠ C" *)
  shows "BetH A B C ∨ ¬ BetH A B C" 
  by blast

lemma cut2_not_cut:
  assumes "¬ ColH A B C" and
    "cut l A B" and
    "cut l A C" 
  shows "¬ cut l B C" 
proof -
  have "¬ IncidL A l" 
    using assms(2) local.cut_def by blast
  have "¬ IncidL B l" 
    using assms(2) local.cut_def by blast
  have "¬ IncidL C l" 
    using assms(3) local.cut_def by blast
  obtain AB where "IncidL AB l" and "BetH A AB B" 
    using assms(2) local.cut_def by blast
  hence "ColH A AB A" 
    using colH_trivial121 by blast
  obtain AC where "IncidL AC l" and "BetH A AC C" 
    using assms(3) local.cut_def by blast
  hence "ColH A AC C" 
    by (simp add: between_col)
  {
    assume "cut l B C"
    then obtain BC where "IncidL BC l" and "BetH B BC C" 
      using local.cut_def by blast
    hence "ColH B BC C" 
      by (simp add: between_col)
    have "ColH AB AC BC" 
      using ColH_def Is_line ‹IncidL AB l› ‹IncidL AC l› ‹IncidL BC l› by blast
    have "AB ≠ AC" 
      using colH_trans ‹BetH A AB B› ‹ColH A AB A› ‹ColH A AC C› assms(1) 
        betH_expand by blast
    have "AB ≠ BC" 
      by (metis ‹BetH A AB B› ‹ColH B BC C› assms(1) betH_colH colH_trans ncolH_distincts)
    have "BC ≠ AC" 
      by (metis ‹BetH A AC C› ‹BetH B BC C› assms(1) betH_colH between_comm 
          colH_trans ncolH_distincts)
    have "BetH AB AC BC ∨ BetH AC BC AB ∨ BetH BC AB AC" 
      using ‹AB ≠ AC› ‹AB ≠ BC› ‹BC ≠ AC› ‹ColH AB AC BC› between_comm between_one by blast
    moreover
    {
      assume "BetH AB AC BC"
      then obtain m where "IncidL A m" and "IncidL C m" 
        using ‹BetH A AC C› betH_line by blast
      have "¬ ColH AB BC B" 
        using ColH_def ‹AB ≠ BC› ‹IncidL AB l› ‹IncidL BC l› ‹¬ IncidL B l›
          inter_incid_uniquenessH by blast
      have "¬ IncidL B m" 
        using Hilbert_neutral_dimensionless_pre.ColH_def Is_line ‹IncidL A m›
          ‹IncidL C m› assms(1) by fastforce
      have "cut m AB BC" 
      proof -
        {
          assume "IncidL AB m"
          hence "ColH A B C" 
            using betH_colH ‹BetH A AB B› ‹IncidL A m› ‹¬ IncidL B m› betH_line
              inter_incid_uniquenessH by blast
          hence ?thesis         
            by (simp add: assms(1))
        }
        moreover
        {
          assume "IncidL BC m"
          hence "ColH A B C" 
            using betH_colH ‹BetH B BC C› ‹IncidL C m› ‹¬ IncidL B m› betH_line
              inter_incid_uniquenessH by blast
          hence ?thesis 
            by (simp add: assms(1))
        }
        moreover have "IncidL AC m" 
          using betH_colH ‹BetH A AC C› ‹IncidL A m› ‹IncidL C m› betH_line 
            inter_incid_uniquenessH by blast
        ultimately show ?thesis
          using Is_line ‹BetH AB AC BC› local.cut_def by blast
      qed
      obtain p where "IncidP AB p" and "IncidP BC p" and "IncidP B p" 
        using ‹¬ ColH AB BC B› plan_existence by blast
      have "(¬ ColH AB BC B ∧ IncidP AB p ∧ IncidP BC p ∧ IncidP B p ∧ 
               IncidLP m p ∧ ¬ IncidL B m ∧ cut m AB BC) ⟶ (cut m AB B ∨ cut m BC B)" 
        using pasch Is_line Is_plane ‹IncidL C m› by blast
      moreover
      have "(¬ ColH AB BC B ∧ IncidP AB p ∧ IncidP BC p ∧ IncidP B p ∧ 
               IncidLP m p ∧ ¬ IncidL B m ∧ cut m AB BC)"
      proof -
        have "IncidLP m p ∧ ¬ IncidL B m ∧ cut m AB BC" 
          by (metis (full_types) Hilbert_neutral_dimensionless.betH_colH 
              Hilbert_neutral_dimensionless_axioms Is_line Is_plane ‹AB ≠ BC› ‹BetH A AC C› 
              ‹BetH B BC C› ‹ColH AB AC BC› ‹IncidL A m› ‹IncidL C m› ‹IncidP AB p› 
              ‹IncidP B p› ‹IncidP BC p› ‹¬ IncidL B m› ‹local.cut m AB BC› betH_line 
              colH_permut_132 inter_incid_uniquenessH line_on_plane line_on_plane')
        thus ?thesis 
          using ‹IncidP AB p› ‹IncidP B p› ‹IncidP BC p› ‹¬ ColH AB BC B› by auto
      qed
      ultimately have "cut m AB B ∨ cut m BC B" by blast
      moreover
      {
        assume "cut m AB B"
        then obtain I where "IncidL I m" and "BetH AB I B" 
          using local.cut_def by blast
        hence "ColH AB I B" 
          using between_col by blast
        have "ColH A I C" 
          using ColH_def Is_line ‹IncidL A m› ‹IncidL C m› ‹IncidL I m› by blast
        {
          assume "A = I"
          hence "¬ BetH A AB B" 
            using ‹A = I› ‹BetH AB I B› between_only_one' by blast
          hence False 
            using ‹BetH A AB B› by blast
        }
        hence "A ≠ I" 
          by blast
        have "ColH A I A" 
          using colH_trivial121 by fastforce
        have "ColH A I B" 
          by (meson ‹BetH A AB B› ‹BetH AB I B› betH_colH betH_trans0 between_comm)
        hence "ColH A B C" 
          using colH_trans ‹A ≠ I› ‹ColH A I A› ‹ColH A I C› by blast
        hence False 
          by (simp add: assms(1))
      }
      moreover
      {
        assume "cut m BC B"
        then obtain C' where "IncidL C' m" and "BetH BC C' B" 
          using local.cut_def by blast 
        have "ColH BC C' B" 
          by (simp add: ‹BetH BC C' B› betH_colH)
        have "B ≠ BC" 
          using ‹IncidL BC l› ‹¬ IncidL B l› by auto
        have "ColH B BC B" 
          using colH_trivial121 by auto
        have "ColH B BC C'" 
          using ‹ColH BC C' B› colH_permut_312 by blast
        have "ColH B C C'" 
          using ‹ColH B BC C› ‹B ≠ BC› ‹ColH B BC B› ‹ColH B BC C'› 
            ‹ColH B BC C› colH_trans by blast
        have "C ≠ C'" 
          using ‹BetH B BC C› ‹BetH BC C' B› between_only_one by blast
        have "ColH A B C" 
          using ColH_def ‹C ≠ C'› ‹ColH B C C'› ‹IncidL C m› ‹IncidL C' m› 
            ‹¬ IncidL B m› inter_incid_uniquenessH by auto
        hence False 
          by (simp add: assms(1))
      }
      ultimately have False 
        by blast
    }
    moreover
    {
      assume "BetH AC BC AB"
      obtain m where "IncidL C m" and "IncidL B m" 
        using ‹BetH B BC C› betH_line by blast
      have "¬ ColH AB AC A" 
        using ColH_def ‹AB ≠ AC› ‹IncidL AB l› ‹IncidL AC l› 
          ‹¬ IncidL A l› inter_incid_uniquenessH by blast
      have "¬ IncidL A m" 
        using ColH_def Is_line ‹IncidL B m› ‹IncidL C m› assms(1) by blast
      have "¬ IncidL AC m" 
        using betH_colH ‹BetH A AC C› ‹IncidL C m› ‹¬ IncidL A m› 
          betH_line inter_incid_uniquenessH by blast
      have "¬ IncidL AB m" 
        using betH_colH ‹BetH A AB B› ‹IncidL B m› ‹¬ IncidL A m› 
          betH_line inter_incid_uniquenessH by blast
      have "IncidL BC m" 
        using betH_colH ‹BetH B BC C› ‹IncidL B m› ‹IncidL C m› 
          betH_line inter_incid_uniquenessH by blast
      hence "cut m AC AB" 
        using Is_line ‹BetH AC BC AB› ‹IncidL BC m› ‹¬ IncidL AB m› 
          ‹¬ IncidL AC m› local.cut_def by blast
      hence "cut m AB AC" 
        using cut_comm by blast
      obtain p where "IncidP AB p" and "IncidP AC p" and "IncidP A p" 
        using ‹¬ ColH AB AC A› plan_existence by blast
      have "(¬ ColH AB AC A ∧ IncidP AB p ∧ IncidP AC p ∧ IncidP A p ∧ 
               IncidLP m p ∧ ¬ IncidL A m ∧ cut m AB AC) ⟶ (cut m AB A ∨ cut m AC A)" 
        using Is_line Is_plane ‹IncidL C m› pasch by blast
      moreover
      have "¬ ColH AB AC A ∧ IncidP AB p ∧ IncidP AC p ∧ IncidP A p ∧ 
              IncidLP m p ∧ ¬ IncidL A m ∧ cut m AB AC" 
      proof -
        have "¬ ColH AB AC A ∧ IncidP AB p ∧ IncidP AC p ∧ IncidP A p" 
          by (simp add: ‹IncidP A p› ‹IncidP AB p› ‹IncidP AC p› ‹¬ ColH AB AC A›)
        moreover have "IncidLP m p ∧ ¬ IncidL A m ∧ cut m AB AC" 
          by (metis (mono_tags, lifting) betH_colH line_on_plane Is_line Is_plane
              ‹AB ≠ AC› ‹BetH A AC C› ‹BetH B BC C› ‹ColH AB AC BC› ‹IncidL BC m› ‹IncidL C m›
              ‹IncidP A p› ‹IncidP AB p› ‹IncidP AC p› ‹¬ IncidL A m› ‹local.cut m AB AC›
              line_on_plane')
        ultimately show ?thesis 
          by blast
      qed
      ultimately have "cut m AB A ∨ cut m AC A" 
        by blast
      moreover {
        assume "cut m AB A"
        obtain B' where "IncidL B' m" and "BetH AB B' A" 
          using ‹local.cut m AB A› local.cut_def by blast
        then have "ColH AB B' A" 
          using betH_colH by force
        have "ColH A B B'" 
          using betH_expand ‹BetH A AB B› ‹ColH A AB A› ‹ColH AB B' A› 
            colH_permut_312 colH_trans by blast
        hence False 
          using ColH_def ‹BetH A AB B› ‹BetH AB B' A› ‹IncidL B m› ‹IncidL B' m› 
            ‹¬ IncidL A m› between_only_one inter_incid_uniquenessH by blast
      }
      moreover {
        assume "cut m AC A"
        then obtain I where "IncidL I m" and "BetH AC I A" 
          using local.cut_def by blast
        hence "ColH AC I A" 
          by (simp add: betH_colH)
        have "ColH C I A" 
          by (metis betH_colH ‹BetH AC I A› ‹ColH A AC C› colH_permut_312 
              colH_trans colH_trivial121)
        hence "ColH A B C" 
          using ColH_def ‹BetH A AC C› ‹BetH AC I A› ‹IncidL C m› ‹IncidL I m›
            ‹¬ IncidL A m› between_only_one inter_incid_uniquenessH by blast
        hence False 
          using assms(1) by fastforce
      }
      ultimately have False 
        by blast
    }
    moreover
    {
      assume "BetH BC AB AC"
      obtain m where "IncidL A m" and "IncidL B m" 
        using ‹BetH A AB B› betH_line by blast
      have "¬ ColH BC A C" 
        by (metis ‹ColH B BC C› ‹IncidL BC l› ‹¬ IncidL C l› assms(1)
            colH_permut_213 colH_trans colH_trivial122)
      have "¬ IncidL C m" 
        using ColH_def Is_line ‹IncidL A m› ‹IncidL B m› assms(1) by blast
      have "cut m BC AC" 
        by (metis (full_types) ncolH_distincts Is_line ‹AB ≠ AC› ‹AB ≠ BC› 
            ‹BetH A AB B› ‹BetH BC AB AC› ‹IncidL A m› ‹IncidL AB l› ‹IncidL AC l›
            ‹IncidL B m› ‹¬ IncidL B l› assms(1) betH_line inter_incid_uniquenessH
            local.cut_def)
      have "¬ IncidL AC m" 
        using ‹local.cut m BC AC› local.cut_def by blast
      obtain p where "IncidP BC p" and "IncidP AC p" and "IncidP C p" 
        using plan_existence
        by (meson ‹BC ≠ AC› line_on_plane' ncolH_exists) 
      have "(¬ ColH BC AC C ∧ IncidP BC p ∧ IncidP AC p ∧ IncidP C p ∧ 
             IncidLP m p ∧ ¬ IncidL C m ∧ cut m BC AC) ⟶ (cut m BC C ∨ cut m AC C)" 
        using Is_line Is_plane ‹IncidL B m› pasch by blast
      moreover have "¬ ColH BC AC C ∧ IncidP BC p ∧ IncidP AC p" 
        using ColH_def ‹BC ≠ AC› ‹IncidL AC l› ‹IncidL BC l› ‹IncidP AC p› 
          ‹IncidP BC p› ‹¬ IncidL C l› inter_incid_uniquenessH by auto
      moreover have "IncidP C p ∧ IncidLP m p ∧ ¬ IncidL C m ∧ cut m BC AC" 
        by (metis ncolH_distincts Is_line Is_plane ‹ColH A AC C› ‹ColH B BC C› 
            ‹IncidL A m› ‹IncidL B m› ‹IncidP C p› ‹¬ IncidL C m› ‹local.cut m BC AC› 
            assms(1) calculation(2) colH_permut_321 line_on_plane line_on_plane') 
      moreover have "¬ cut m BC C" 
        by (meson ‹BetH B BC C› ‹IncidL B m› betH_trans0 between_comm local.cut_def
            outH_def out_same_side same_side_def)
      moreover have "¬ cut m AC C" 
        by (meson ‹BetH A AC C› ‹IncidL A m› betH_trans0 between_comm local.cut_def
            outH_def out_same_side same_side_def)
      ultimately have False 
        by blast
    }
    ultimately
    have False 
      by blast
  }
  thus ?thesis 
    by blast
qed

lemma strong_pasch:
  assumes "¬ ColH A B C" and
    "IncidP A p" and 
    "IncidP B p" and
    "IncidP C p" and
    "IncidLP l p" and
    "¬ IncidL C l" and
    "cut l A B"
  shows "(cut l A C ∧ ¬ cut l B C) ∨ (cut l B C ∧ ¬ cut l A C)"
  by (meson cut2_not_cut IncidLP_def assms(1) assms(2) assms(3) assms(4) 
      assms(5) assms(6) assms(7) pasch)

lemma out2_out: 
  assumes "C ≠ D" and
    "BetH A B C" and
    "BetH A B D"
  shows "BetH B C D ∨ BetH B D C" 
proof -
  have "A ≠ B" 
    using assms(2) betH_distincts by blast
  have "ColH A B B" 
    by (simp add: colH_trivial122)
  have "ColH A B C" 
    by (simp add: assms(2) between_col)
  have "ColH A B D" 
    by (simp add: assms(3) betH_colH)
  hence "ColH B C D" 
    using colH_trans ‹A ≠ B› ‹ColH A B B› ‹ColH A B C› by blast
  {
    assume "BetH C D B"
    hence ?thesis 
      using between_comm by blast
  }
  moreover
  {
    assume "BetH C B D"
    have "ColH A C D" 
      using ‹A ≠ B› ‹ColH A B C› ‹ColH A B D› colH_trans colH_trivial121 by blast
    moreover have "BetH A C D ⟶ ?thesis" 
      using assms(2) betH_trans0 by blast
    moreover have "BetH C D A ⟶ ?thesis" 
      using assms(3) betH_trans0 between_comm by blast
    moreover have "BetH C A D ⟶ ?thesis" 
      using assms(2) assms(3) betH_trans0 between_comm between_only_one' by blast
    ultimately have ?thesis 
      by (metis assms(1) assms(2) assms(3) betH_colH between_one)
  }
  ultimately show ?thesis 
    by (metis ‹ColH B C D› assms(1) assms(2) assms(3) betH_distincts between_one)
qed

lemma out2_out1: 
  assumes "C ≠ D" and 
    "BetH A B C" and
    "BetH A B D" 
  shows "BetH A C D ∨ BetH A D C" 
  by (meson assms(1) assms(2) assms(3) betH_trans out2_out)

lemma betH2_out:
  assumes "B ≠ C" and
    "BetH A B D" and
    "BetH A C D"
  shows "BetH A B C ∨ BetH A C B" 
proof -
  have "A ≠ D" 
    using assms(2) between_diff by auto
  moreover have "ColH A D A" 
    by (simp add: colH_trivial121)
  moreover have "ColH A D B" 
    by (simp add: assms(2) betH_colH colH_permut_132)
  moreover have "ColH A D C" 
    using assms(3) betH_colH colH_permut_132 by blast
  ultimately have "ColH A B C" 
    using colH_trans by blast
  moreover have "BetH B C A ⟶ ?thesis" 
    using between_comm by blast
  moreover have "BetH C A B ⟶ ?thesis" 
    using assms(2) assms(3) betH_trans2 between_only_one' by blast
  ultimately show ?thesis 
    by (metis assms(1) assms(2) assms(3) betH_colH between_comm between_one)
qed

lemma segment_construction:
  shows "∃ E. Bet A B E ∧ Cong B E C D"
proof (cases "C = D")
  case True
  thus ?thesis
    using Bet_def Cong_def by force
next
  case False
  hence "C ≠ D"
    by blast
  {
    assume "A = B"
    hence ?thesis 
      by (metis Bet_def Cong_def betH_distincts cong_existence' line_existence)
  }
  moreover
  {
    assume "A ≠ B"
    obtain l where "IncidL A l" and "IncidL B l"
      using ‹A ≠ B› line_existence by auto
    obtain F where "∃ B'. IncidL F l ∧ IncidL B' l ∧ BetH F B B' ∧ CongH B F C D ∧ CongH B B' C D" 
      using False ‹IncidL B l› cong_existence' by presburger
    then obtain F' where "IncidL F l" and "IncidL F' l" and "BetH F B F'" and
      "CongH B F C D" and "CongH B F' C D"
      by blast
    hence "ColH A F F'" 
      using ColH_def Is_line ‹IncidL A l› by blast
    have "A = F ⟶ ?thesis" 
      by (metis Bet_def Cong_def ‹BetH F B F'› ‹CongH B F' C D› betH_distincts)
    moreover {
      assume "A ≠ F"
      have "A = F' ⟶ ?thesis" 
        by (metis Bet_def Cong_def ‹BetH F B F'› ‹CongH B F C D› betH_distincts between_comm)
      moreover
      {
        assume "A ≠ F'"
        have "ColH A F F'" 
          using ‹ColH A F F'› by blast
        have "BetH A F F' ⟶ ?thesis" 
          by (metis Cong_def False ‹BetH F B F'› ‹CongH B F' C D› betH_to_bet
              betH_trans0 between_comm)
        moreover have "BetH F F' A ⟶ ?thesis" 
          by (metis Bet_def Cong_def False ‹BetH F B F'› ‹CongH B F C D› 
              betH_distincts betH_trans0 between_comm)
        moreover have "BetH F' A F ⟶ ?thesis" 
          by (metis (full_types) Cong_def False ‹A ≠ B› ‹BetH F B F'› ‹CongH B F C D›
              ‹CongH B F' C D› betH2_out betH_to_bet between_comm between_only_one out2_out)
        ultimately have ?thesis 
          by (metis between_one ‹A = F ⟶ (∃E. Bet A B E ∧ Cong B E C D)› 
              ‹A = F' ⟶ (∃E. Bet A B E ∧ Cong B E C D)› ‹BetH F B F'› ‹ColH A F F'› 
              between_comm between_diff)
      }
      ultimately have  ?thesis 
        by blast
    }
    ultimately have ?thesis 
      by blast
  }
  ultimately show ?thesis 
    by blast
qed

lemma lower_dim_e:
  shows "∃ A B C. ¬ (Bet A B C ∨ Bet B C A ∨ Bet C A B)" 
  by (meson bet_colH colH_permut_312 lower_dim_2)

lemma outH_dec:
  shows "outH A B C ∨ ¬ outH A B C" 
  by simp

lemma out_construction: 
  assumes "X ≠ Y" and
    "A ≠ B"
  shows "∃ C. CongH A C X Y ∧ outH A B C" 
  by (metis assms(1) assms(2) cong_existence line_existence)

lemma segment_constructionH:
  assumes "A ≠ B" and 
    "C ≠ D"
  shows "∃ E. BetH A B E ∧ CongH B E C D" 
  by (metis Bet_def Cong_def assms(1) assms(2) segment_construction)

lemma EqL_dec: 
  shows "EqL l m ∨ ¬ EqL l m" 
  by simp

lemma cut_exists: 
  assumes "IsL l" and (*ROLL ADD*)
    "¬ IncidL A l"
  shows "∃ B. cut l A B" 
  using assms(1) assms(2) same_side_def same_side_refl by blast

lemma outH_col: 
  assumes "outH A B C"
  shows "ColH A B C" 
  by (simp add: assms outH_expand)

lemma cut_distinct: 
  assumes "cut l A B"
  shows "A ≠ B" 
  using assms local.cut_def not_betH121 by fastforce

lemma same_side_not_cut: 
  assumes "same_side A B l"
  shows "¬ cut l A B"
proof -
  obtain P where "cut l A P" and "cut l B P" 
    using assms same_side_def by blast
  {
    assume "ColH P A B"
    {
      assume "cut l A B"
      obtain M where "IncidL M l" and "BetH A M P" 
        using ‹local.cut l A P› local.cut_def by blast
      obtain N where "IncidL N l" and "BetH B N P" 
        using ‹local.cut l B P› local.cut_def by blast
      {
        assume "M = N"
        hence "BetH M A B ∨ BetH M B A" 
          using ‹BetH A M P› ‹BetH B N P› ‹local.cut l A B› between_comm 
            cut_distinct out2_out by blast
        obtain Q where "IncidL Q l" and "BetH A Q B" 
          using ‹local.cut l A B› local.cut_def by blast
        obtain R where "IncidL R l" and "BetH A R B" 
          using ‹BetH A Q B› ‹IncidL Q l› by blast
        have "ColH A B M" 
          using ‹BetH M A B ∨ BetH M B A› betH_colH between_comm colH_permut_231 by blast
        obtain m where "IncidL A m" and "IncidL B m" 
          using ‹BetH A Q B› betH_line by blast
        obtain mm where "IncidL P mm" and "IncidL A mm" and "IncidL B mm" 
          using ColH_def ‹ColH P A B› by blast
        have "EqL m mm" 
          by (metis Is_line ‹IncidL A m› ‹IncidL A mm› ‹IncidL B m› ‹IncidL B mm› 
              ‹⋀thesis. (⋀R. ⟦IncidL R l; BetH A R B⟧ ⟹ thesis) ⟹ thesis› 
              betH_colH line_uniqueness)
        obtain nn where "IncidL A nn" and "IncidL R nn" and "IncidL B nn" 
          using ‹BetH A R B› betH_line by blast
        have "EqL m nn" 
          by (metis Is_line ‹BetH A R B› ‹IncidL A m› ‹IncidL A nn› ‹IncidL B m›
              ‹IncidL B nn› line_uniqueness not_betH121)
        obtain pp where "IncidL A pp" and "IncidL B pp" and "IncidL M pp" 
          using ColH_def ‹ColH A B M› by blast
        have "EqL m pp" 
          by (metis Is_line ‹BetH M A B ∨ BetH M B A› ‹IncidL A m› ‹IncidL A pp› 
              ‹IncidL B m› ‹IncidL B pp› betH_distincts line_uniqueness)
        have "R = M" 
          by (metis betH_colH ‹IncidL A nn› ‹IncidL A pp› ‹IncidL B nn› 
              ‹IncidL B pp› ‹IncidL M l› ‹IncidL M pp› ‹IncidL R l› ‹IncidL R nn› 
              ‹local.cut l A B› inter_incid_uniquenessH local.cut_def)
        have "BetH M A B ⟶ False" 
          using ‹BetH A R B› ‹R = M› between_only_one' by blast
        moreover have "BetH M B A ⟶ False" 
          using ‹BetH A R B› ‹R = M› between_only_one by blast
        ultimately have False 
          using ‹BetH M A B ∨ BetH M B A› by blast
      }
      hence "M ≠ N" 
        by blast
      have "A ≠ B" 
        using ‹local.cut l A B› cut_distinct by auto
      obtain T where "IncidL T l" and "BetH A T B" 
        using ‹local.cut l A B› local.cut_def by blast
      obtain m where "IncidL P m" and "IncidL A m" and "IncidL B m" 
        using ColH_def ‹ColH P A B› by blast
      obtain mm where "IncidL A mm" and "IncidL M mm" and "IncidL P mm"
        using ‹BetH A M P› betH_line by blast
      obtain nn where "IncidL B nn" and "IncidL N nn" and "IncidL P nn"
        using ‹BetH B N P› betH_line by blast
      have "M = N" using inter_incid_uniquenessH 
        by (metis Hilbert_neutral_dimensionless_pre.cut_def ‹BetH B N P› 
            ‹IncidL A m› ‹IncidL A mm› ‹IncidL B m› ‹IncidL M l› ‹IncidL M mm› 
            ‹IncidL N l› ‹IncidL P m› ‹IncidL P mm› 
            ‹⋀thesis. (⋀nn. ⟦IncidL B nn; IncidL N nn; IncidL P nn⟧ ⟹ thesis) ⟹ thesis› 
            ‹local.cut l A P› betH_expand)
      hence False 
        by (simp add: ‹M ≠ N›)
    }
    hence "¬ cut l A B" 
      by blast
  }
  moreover
  {
    assume "¬ ColH P A B"
    hence ?thesis 
      using ‹local.cut l A P› ‹local.cut l B P› cut2_not_cut cut_comm by blast
  }
  ultimately show ?thesis 
    by blast
qed

lemma IncidLP_morphism:
  assumes 
    "IsL m" and
    "IsP q" and
    "IncidLP l p" and
    "EqL l m" and
    "EqP p q"
  shows "IncidLP m q" 
proof -
  {
    fix A
    assume "IncidL A m"
    have "IncidP A q" 
      by (metis Hilbert_neutral_dimensionless_pre.IncidLP_def IncidP_morphism 
          ‹IncidL A m› assms(1) assms(2) assms(3) assms(4) assms(5) morph)
  }
  thus ?thesis 
    using IncidLP_def assms(1) assms(2) by blast
qed

lemma same_side__plane:
  assumes "same_side A B l" 
  shows "∃ p. IncidP A p ∧ IncidP B p ∧ IncidLP l p" 
proof -
  obtain P where "cut l A P" and "cut l B P" 
    using assms same_side_def by blast 
  then obtain X where "IncidL X l" and "BetH A X P" 
    using local.cut_def by blast
  {
    assume "ColH A B P"
    obtain Y where "X ≠ Y" and "IncidL Y l" 
      using ‹IncidL X l› other_point_on_line by blast
    {
      assume "ColH X Y A"
      obtain m where "IncidL X m" and "IncidL Y m" and "IncidL A m" 
        using ColH_def ‹ColH X Y A› by auto
      hence "X = Y" 
        using inter_incid_uniquenessH ‹IncidL X l› ‹IncidL Y l› ‹local.cut l A P› 
          local.cut_def by blast
      hence False 
        by (simp add: ‹X ≠ Y›)
    }
    hence "¬ ColH X Y A" 
      by blast
    obtain p where "IncidP X p" and "IncidP Y p" and "IncidP A p" 
      using ‹ColH X Y A ⟹ False› plan_existence by blast
    hence ?thesis 
      by (metis betH_colH Is_line Is_plane ‹BetH A X P› ‹ColH A B P› 
          ‹IncidL X l› ‹IncidL Y l› ‹X ≠ Y› colH_permut_132 line_on_plane line_on_plane')
  }
  moreover 
  {
    assume "¬ ColH A B P"
    obtain p where "IncidP A p" and "IncidP B p" and "IncidP P p" 
      using ‹¬ ColH A B P› plan_existence by blast
    obtain Y where "IncidL Y l" and "BetH B Y P" 
      using ‹local.cut l B P› local.cut_def by blast
    have "IncidP X p" 
      by (metis ncolH_distincts ‹BetH A X P› ‹IncidP A p› ‹IncidP P p› 
          ‹¬ ColH A B P› between_col colH_permut_132 line_on_plane')
    moreover have "IncidP Y p" 
      using ‹BetH B Y P› ‹IncidP B p› ‹IncidP P p› betH_colH colH_permut_132 
        line_on_plane' by blast
    ultimately have "IncidLP l p" using line_on_plane 
      by (metis Is_line Is_plane ‹BetH A X P› ‹BetH B Y P› ‹IncidL X l› 
          ‹IncidL Y l› ‹¬ ColH A B P› between_col between_comm colH_permut_231 
          colH_trivial112 out2_out1)
    hence ?thesis 
      using ‹IncidP A p› ‹IncidP B p› by blast
  }
  ultimately show ?thesis 
    by blast
qed

lemma same_side_prime__plane:
  assumes "same_side' A B C D"
  shows "∃ p. IncidP A p ∧ IncidP B p ∧ IncidP C p ∧ IncidP D p"
proof -
  obtain l where "IsL l" and "IncidL C l" and "IncidL D l" 
    by (metis line_existence lower_dim_2)
  obtain p where "IsP p" and "IncidP A p" and "IncidP B p" and "IncidLP l p" 
    by (meson Is_plane ‹IncidL C l› ‹IncidL D l› ‹IsL l› assms 
        same_side'_def same_side__plane)
  thus ?thesis 
    using IncidLP_def ‹IncidL C l› ‹IncidL D l› by blast
qed

lemma cut_same_side_cut:
  assumes "cut l P X" and
    "same_side X Y l"
  shows "cut l P Y" 
proof -
  have "¬ cut l X Y" 
    by (simp add: assms(2) same_side_not_cut)
  have  "X = Y ⟶ ?thesis" 
    using assms(1) by fastforce
  moreover {
    assume "X ≠ Y"
    obtain A where "IncidL A l" and "BetH P A X" 
      using assms(1) local.cut_def by blast
    {
      assume "ColH P X Y"
      {
        assume "IncidL Y l"
        hence False 
          using ‹IncidL Y l› assms(2) local.cut_def same_side_def by force
      }
      hence "¬ IncidL Y l" 
        by blast
      have "IncidL A l" 
        by (simp add: ‹IncidL A l›)
      moreover have "BetH P A Y" 
      proof -
        have "BetH P X Y ⟶ BetH P A Y" 
          using ‹BetH P A X› betH_trans0 by blast
        moreover have "BetH X Y P ⟶ BetH P A Y" 
          by (metis ‹BetH P A X› ‹IncidL A l› ‹¬ IncidL Y l› ‹¬ local.cut l X Y› 
              assms(1) betH2_out betH_trans0 between_comm local.cut_def)
        moreover have "BetH X P Y ⟶ BetH P A Y" 
          by (meson ‹¬ IncidL Y l› ‹¬ local.cut l X Y› assms(1) betH_trans0 
              between_comm local.cut_def)
        ultimately show ?thesis 
          by (metis betH_to_bet between_one cut_comm ‹BetH P A X› ‹ColH P X Y›
              ‹¬ local.cut l X Y› assms(1))
      qed
      ultimately have ?thesis 
        using ‹¬ IncidL Y l› assms(1) local.cut_def by blast
    }
    moreover
    {
      assume "¬ ColH P X Y"
      {
        assume "IncidL Y l"
        obtain T where "cut l X T" and "cut l Y T" 
          using assms(2) same_side_def by blast
        hence False 
          using ‹IncidL Y l› local.cut_def by blast
      }
      hence "¬ IncidL Y l" 
        by blast
      obtain p where "IncidP P p" and "IncidP X p" and "IncidP Y p" 
        using ‹¬ ColH P X Y› plan_existence by blast
      have "cut l X Y ∨ cut l P Y" 
      proof -
        let ?A="X"
        let ?B="P"
        let ?C="Y"
        have "¬ ColH ?A ?B ?C" 
          using ‹¬ ColH P X Y› colH_permut_213 by blast
        moreover have "IsL l" 
          using assms(2) same_side_def by blast
        moreover have "IsP p" 
          using Is_plane ‹IncidP P p› by blast
        moreover have "IncidP ?A p" 
          by (simp add: ‹IncidP X p›)
        moreover have "IncidP ?B p" 
          using ‹IncidP P p› by auto
        moreover have "IncidP ?C p" 
          by (simp add: ‹IncidP Y p›)
        moreover have "IncidLP l p" 
        proof -
          {
            fix A'
            assume "IncidL A' l"
            have "ColH P A X" 
              by (simp add: ‹BetH P A X› between_col)

            obtain I where "IncidL I l" and "BetH P I X" 
              by (meson ‹⋀thesis. (⋀A. ⟦IncidL A l; BetH P A X⟧ ⟹ thesis) ⟹ thesis›)
            hence "ColH P I X" 
              using between_col by blast
            have "I = A' ⟶ IncidP A' p" 
              by (metis betH_colH ‹BetH P I X› calculation(4) calculation(5) 
                  colH_permut_132 line_on_plane')
            moreover 
            obtain p' where "IsP p'" and "IncidP X p'" and "IncidP Y p'" and "IncidLP l p'" 
              using Is_plane assms(2) same_side__plane by blast
            have "IncidP P p'" 
              using IncidLP_def ‹BetH P A X› ‹ColH P A X› ‹IncidL A l› 
                ‹IncidLP l p'› ‹IncidP X p'› betH_distincts colH_permut_231 
                line_on_plane' by blast
            have "IncidP A' p'" 
              using IncidLP_def ‹IncidL A' l› ‹IncidLP l p'› by blast
            have "IncidP A p'" 
              using IncidLP_def ‹IncidL A l› ‹IncidLP l p'› by blast
            have "EqP p p'" 
              by (meson plane_uniqueness ‹IncidP P p'› ‹IncidP P p› 
                  ‹IncidP X p'› ‹IncidP X p› ‹IncidP Y p'› ‹IncidP Y p› ‹IsP p'› 
                  ‹IsP p› ‹¬ ColH P X Y›)
            hence "IncidP A' p" 
              by (meson EqP_sym IncidP_morphism ‹IncidP A' p'› ‹IsP p'› ‹IsP p›)
          }
          thus ?thesis 
            using IncidLP_def calculation(2) calculation(3) by blast
        qed
        moreover have "¬ IncidL ?C l"
          by (simp add: ‹¬ IncidL Y l›)
        moreover have "cut l ?A ?B" 
          by (simp add: assms(1) cut_comm)
        ultimately
        show ?thesis using pasch by blast
      qed
      have "IncidP A p" 
        using betH_colH ‹BetH P A X› ‹IncidP P p› ‹IncidP X p› colH_permut_132 
          line_on_plane' by blast
      obtain q where "IncidP X q" and "IncidP Y q" and "IncidLP l q" 
        using assms(2) same_side__plane by blast
      have "IncidP P q" 
        using line_on_plane' [of _ _ p P]
        by (metis (mono_tags, lifting) Hilbert_neutral_dimensionless_pre.IncidLP_def ‹BetH P A X›
            ‹IncidL A l› ‹IncidLP l q› ‹IncidP X q› betH_colH between_comm line_on_plane') 
      have "EqP p q" 
        using Is_plane ‹IncidP P p› ‹IncidP P q› ‹IncidP X p› ‹IncidP X q› 
          ‹IncidP Y p› ‹IncidP Y q› ‹¬ ColH P X Y› plane_uniqueness by presburger
      hence "IncidLP l p" 
        by (meson EqL_refl EqP_sym IncidLP_morphism Is_line Is_plane 
            ‹IncidL A l› ‹IncidLP l q› ‹IncidP P p›)
      have ?thesis 
        using ‹¬ local.cut l X Y› ‹local.cut l X Y ∨ local.cut l P Y› by blast
    }
    ultimately have ?thesis 
      by blast
  }
  ultimately show ?thesis
    by blast
qed

(** Theorem 11 of Hilbert: the angles at the base of an isosceles triangle are congruent *)

lemma isosceles_congaH: 
  assumes "¬ ColH A B C" and
    "CongH A B A C"
  shows "CongaH A B C A C B" 
  by (metis assms(1) assms(2) colH_permut_213 colH_permut_312 colH_trivial112 
      congH_sym cong_5 conga_comm)

lemma cong_distincts:
  assumes "A ≠ B" and
    "Cong A B C D"
  shows "C ≠ D" 
  using assms(1) assms(2) cong_identity by blast

lemma cong_sym:
  assumes "Cong A B C D"
  shows "Cong C D A B" 
  using Cong_def assms congH_sym by presburger

lemma cong_trans: 
  assumes "Cong A B C D" and
    "Cong C D E F"
  shows "Cong A B E F" 
  by (meson assms(1) assms(2) cong_inner_transitivity cong_sym)

lemma betH_not_congH:
  assumes "BetH A B C"
  shows "¬ CongH A B A C" 
  by (metis assms betH_expand betH_trans between_comm between_out construction_uniqueness)

lemma congH_permlr: 
  assumes (*"A ≠ B" and*)
    "C ≠ D" and
    "CongH A B C D"
  shows "CongH B A D C" 
  by (metis assms(2) assms(1) congH_sym cong_permr)

lemma congH_perms:
  assumes "A ≠ B" and
    "C ≠ D" and
    "CongH A B C D"
  shows "CongH B A C D ∧ CongH A B D C ∧ CongH C D A B ∧
CongH D C A B ∧ CongH C D B A ∧ CongH D C B A ∧ CongH B A D C" 
  using assms(1) assms(2) assms(3) congH_sym cong_permr by presburger

lemma congH_perml:
  assumes (*"A ≠ B" and*)
    "C ≠ D" and
    "CongH A B C D"
  shows "CongH B A C D" 
  by (metis assms(2) assms(1) congH_perms)

lemma bet_cong3_bet:
  assumes "A' ≠ B'" and
    "B' ≠ C'" and
    "A' ≠ C'" and
    "BetH A B C" and
    "ColH A' B' C'" and
    "CongH A B A' B'" and
    "CongH B C B' C'" and
    "CongH A C A' C'"
  shows "BetH A' B' C'" 
proof -
  {
    assume "BetH B' C' A'"
    obtain B'' where "BetH B C B''" and "CongH C B'' B C" 
      using assms(4) betH_to_bet segment_constructionH by blast
    have "BetH A B B'' ∧ BetH A C B''" 
      using betH_trans ‹BetH B C B''› assms(4) by blast
    hence "BetH A B B''" 
      by blast
    have "BetH A C B''" 
      using ‹BetH A B B'' ∧ BetH A C B''› by blast
    have "CongH A B'' A' B'"
    proof -
      have "ColH A C B''"       
        by (simp add: ‹BetH A C B''› between_col)
      moreover have "disjoint A C C B''"       
        by (simp add: ‹BetH A C B''› bet_disjoint)
      moreover have "disjoint A' C' C' B'"       
        by (simp add: ‹BetH B' C' A'› bet_disjoint between_comm)
      moreover have "CongH C B'' C' B'"       
        by (metis betH_to_bet congH_sym ‹BetH B C B''› ‹CongH C B'' B C› 
            assms(7) cong_permr cong_pseudo_transitivity)
      ultimately show ?thesis
        using addition assms(5) assms(8) colH_permut_132 by blast
    qed
    have "CongH A B'' A B" 
      by (metis ‹BetH A B B'' ∧ BetH A C B''› ‹CongH A B'' A' B'› assms(6) 
          betH_colH congH_sym cong_pseudo_transitivity)
    have "¬ CongH A B A B''" 
      by (simp add: ‹BetH A B B''› betH_not_congH)
    have "CongH A B A B''" 
      using ‹BetH A B B''› ‹CongH A B'' A B› betH_to_bet congH_sym by blast
    hence False 
      by (simp add: ‹¬ CongH A B A B''›)
    hence ?thesis 
      by blast
  }
  moreover 
  {
    assume "BetH C' A' B'"
    obtain B'' where "BetH C A B''" and "CongH A B'' A B" 
      by (metis assms(4) betH_expand segment_constructionH)
    have "CongH C B'' C' B'"
    proof -
      have "disjoint C A A B''"         
        using ‹BetH C A B''› bet_disjoint by force
      moreover have "disjoint C' A' A' B'"         
        by (simp add: ‹BetH C' A' B'› bet_disjoint)
      moreover have "CongH C A C' A'"         
        by (simp add: assms(3) assms(8) congH_permlr)
      moreover have "CongH A B'' A' B'"         
        by (metis ‹BetH C A B''› ‹CongH A B'' A B› assms(6) betH_distincts 
            congH_sym cong_pseudo_transitivity)
      ultimately show ?thesis
        using ‹BetH C A B''› ‹BetH C' A' B'› addition_betH by blast
    qed
    have "BetH B A B'' ∧ BetH C B B''" 
      using betH_trans0 ‹BetH C A B''› assms(4) between_comm by blast
    hence "BetH B A B''"  
      by blast
    have "BetH C B B''" 
      using ‹BetH B A B'' ∧ BetH C B B''› by auto
    have "¬ CongH C B C B''" 
      by (simp add: ‹BetH C B B''› betH_not_congH)
    hence ?thesis 
      by (metis betH_colH ‹BetH C B B''› ‹CongH C B'' C' B'› assms(2) 
          assms(7) congH_perms cong_pseudo_transitivity)
  }
  ultimately show ?thesis 
    using assms(1) assms(2) assms(3) assms(5) between_comm between_one by blast
qed

lemma betH_congH3_outH_betH:
  assumes "BetH A B C" and
    "outH A' B' C'" and
    "CongH A C A' C'" and
    "CongH A B A' B'"
  shows "BetH A' B' C'" 
proof -
  {
    assume "BetH A' C' B'"
    obtain C'' where "BetH A' B' C''" and "CongH B' C'' B C" 
      using ‹BetH A' C' B'› assms(1) betH_distincts segment_constructionH by blast
    hence "CongH A' C'' A C" 
      using addition_betH assms(1) assms(4) betH_distincts congH_sym by presburger
    have "BetH C' B' C'' ∧ BetH A' C' C''" 
      using ‹BetH A' B' C''› ‹BetH A' C' B'› betH_trans0 by blast
    hence "¬ CongH A' C' A' C''" 
      by (simp add: betH_not_congH)
    moreover
    have "CongH A' C' A' C''" 
      by (metis betH_colH congH_sym ‹BetH A' B' C''› ‹CongH A' C'' A C› 
          assms(3) cong_pseudo_transitivity)
    ultimately have ?thesis 
      by simp
  }
  moreover have "(A' ≠ B' ∧ B' ≠ C') ⟶ ?thesis" 
    using assms(2) calculation outH_def by auto
  ultimately show ?thesis 
    by (metis betH_distincts assms(1) assms(2) assms(3) assms(4) betH_not_congH 
        congH_sym cong_pseudo_transitivity outH_def)
qed

lemma outH_sym:
  assumes "A ≠ C" and
    "outH A B C"
  shows "outH A C B" 
  using assms(2) outH_def by fastforce

lemma soustraction_betH:
  assumes "BetH A B C" and
    "BetH A' B' C'" and
    "CongH A B A' B'" and
    "CongH A C A' C'"
  shows "CongH B C B' C'" 
proof -
  obtain C1 where "BetH A' B' C1" and "CongH B' C1 B C" 
    using assms(1) assms(2) betH_to_bet segment_constructionH by blast
  hence "CongH A C A' C1" 
    using addition_betH assms(1) assms(3) betH_distincts congH_sym by presburger
  obtain X where "BetH B A X" 
    by (metis assms(1) between_out)
  obtain X' where "BetH B' A' X'" 
    by (metis assms(2) between_out)
  have "BetH X A C" 
    using ‹BetH B A X› assms(1) betH_trans between_comm by blast
  have "BetH X' A' C1" 
    using ‹BetH A' B' C1› ‹BetH B' A' X'› betH_trans between_comm by blast
  have "C' = C1" 
    by (meson ‹BetH A' B' C1› ‹CongH A C A' C1› assms(2) assms(4) 
        betH_not_congH cong_pseudo_transitivity out2_out1)
  thus ?thesis 
    using ‹BetH A' B' C1› ‹CongH B' C1 B C› betH_colH congH_sym by blast
qed

lemma ncolH_expand:
  assumes "¬ ColH A B C" 
  shows "¬ ColH A B C ∧ A ≠ B ∧ B ≠ C ∧ A ≠ C" 
  using assms colH_trivial112 colH_trivial121 colH_trivial122 by blast

lemma betH_outH__outH:
  assumes "BetH A B C" and
    "outH B C D"
  shows "outH A C D" 
  by (metis betH_expand betH_outH2__betH betH_trans1 
      Hilbert_neutral_dimensionless_pre.outH_def assms(1) assms(2))

(** First case of congruence of triangles *)

lemma th12:
  assumes "¬ ColH A B C" and
    "¬ ColH A' B' C'" and
    "CongH A B A' B'" and
    "CongH A C A' C'" and
    "CongaH B A C B' A' C'"
  shows "CongaH A B C A' B' C' ∧ CongaH A C B A' C' B' ∧ CongH B C B' C'" 
proof (intro conjI)
  show "CongaH A B C A' B' C'" 
    by (simp add: assms(1) assms(2) assms(3) assms(4) assms(5) cong_5)
  show "CongaH A C B A' C' B'" 
    by (meson assms(1) assms(2) assms(3) assms(4) assms(5) colH_permut_132 
        cong_5 conga_permlr)
  obtain D' where "CongH B' D' B C" and "outH B' C' D'" 
    by (metis assms(1) assms(2) colH_trivial122 out_construction)
  show "CongH B C B' C'" 
  proof (cases "B' = D'")
    case True
    thus ?thesis 
      using ‹outH B' C' D'› outH_expand by blast
  next
    case False
    hence "B' ≠ D'"
      by simp
    have "¬ ColH B A C" 
      using assms(1) colH_permut_213 by blast
    moreover have "¬ ColH B' A' D'" 
      using ColH_def ‹outH B' C' D'› assms(2) inter_incid_uniquenessH 
        outH_expand by fastforce
    moreover have "CongH B A B' A'" 
      by (metis assms(3) calculation(2) congH_permlr ncolH_distincts)
    moreover have "CongH B C B' D'" 
      by (simp add: False ‹CongH B' D' B C› congH_sym)
    moreover have "CongaH A B C A' B' D'" 
      using ‹CongaH A B C A' B' C'› ‹outH B' C' D'› calculation(1) calculation(2) 
        conga_out_conga ncolH_expand outH_trivial by blast
    ultimately have "CongaH B A C B' A' D'" 
      using cong_5 by blast
    have "¬ ColH C' A' B'" 
      using assms(2) colH_permut_231 by blast
    moreover have "¬ ColH B A C" 
      using ‹¬ ColH B A C› by blast
    moreover have "same_side' C' C' A' B'" 
      using assms(2) same_side_prime_refl by blast
    moreover have "same_side' C' D' A' B'" 
      by (metis (no_types, lifting) ColH_def ncolH_distincts ‹outH B' C' D'›
          assms(2) out_same_side same_side'_def)
    ultimately have "outH A' C' D'" 
      using ‹CongaH B A C B' A' D'› assms(5) cong_4_uniqueness by presburger
    have "C' = D'" 
      by (metis (full_types) colH_trivial121 outH_expand ‹¬ ColH C' A' B'› 
          ‹outH A' C' D'› ‹outH B' C' D'› colH_permut_213 inter_uniquenessH)
    thus ?thesis 
      by (simp add: ‹CongH B C B' D'›)
  qed
qed

lemma th14:
  assumes "¬ ColH A B C" and
    "¬ ColH A' B' C'" and
    "CongaH A B C A' B' C'" and
    "BetH A B D" and
    "BetH A' B' D'"
  shows "CongaH C B D C' B' D'" 
proof -
  obtain A'' where "CongH B' A'' A B" and "outH B' A' A''" 
    by (metis assms(4) assms(5) betH_distincts out_construction)
  obtain C'' where "CongH B' C'' B C" and "outH B' C' C''" 
    by (metis assms(1) assms(2) colH_trivial122 out_construction)
  obtain D'' where "CongH B' D'' B D" and "outH B' D' D''" 
    using assms(4) assms(5) betH_expand out_construction by blast
  have "CongaH B A C B' A'' C'' ∧ CongaH B C A B' C'' A'' ∧ CongH A C A'' C''" 
  proof (rule th12)
    show "¬ ColH B A C" 
      using assms(1) colH_permut_213 by blast
    show "¬ ColH B' A'' C''" 
      by (metis (mono_tags, opaque_lifting) ‹outH B' A' A''› ‹outH B' C' C''› 
          assms(2) colH_trans colH_trivial121 colH_trivial122 outH_expand)
    show "CongH B A B' A''" 
      by (metis ‹CongH B' A'' A B› ‹outH B' A' A''› congH_perms congH_sym out_distinct)
    show "CongH B C B' C''" 
      using ‹CongH B' C'' B C› ‹outH B' C' C''› congH_sym out_distinct by presburger
    show "CongaH A B C A'' B' C''" 
      using ‹¬ ColH B A C› ‹outH B' A' A''› ‹outH B' C' C''› assms(3) 
        conga_out_conga ncolH_distincts outH_trivial by blast
  qed
  have "BetH A'' B' D''" 
    using ‹outH B' A' A''› ‹outH B' D' D''› assms(5) betH_outH2__betH by blast
  have "CongH A D A'' D''" 
    by (metis (full_types) ‹BetH A'' B' D''› ‹CongH B' A'' A B› 
        ‹CongH B' D'' B D› addition_betH assms(1) assms(4) colH_trivial112 
        congH_perml congH_sym not_betH121)
  {
    assume "ColH A C D"
    have "A ≠ D" 
      using between_diff assms(4) by blast
    moreover have "ColH A D A" 
      by (simp add: colH_trivial121)
    moreover have "ColH A D B" 
      by (simp add: assms(4) between_col colH_permut_132)
    moreover have "ColH A D C" 
      by (simp add: ‹ColH A C D› colH_permut_132)
    hence False 
      using assms(1) calculation(1) calculation(2) calculation(3) colH_trans by blast
  }
  hence "¬ ColH A C D" 
    by blast
  {
    assume "ColH A'' C'' D''"
    have "ColH B' A' A'' ∧ B' ≠ A'' ∧ B' ≠ A'" 
      using ‹outH B' A' A''› outH_expand by blast 
    hence "ColH B' A' A''" 
      by simp
    moreover have "B' ≠ A''" 
      using ‹ColH B' A' A'' ∧ B' ≠ A'' ∧ B' ≠ A'› by blast
    moreover have "B' ≠ A'"
      by (simp add: ‹ColH B' A' A'' ∧ B' ≠ A'' ∧ B' ≠ A'›) 
    moreover have "ColH B' C' C'' ∧ B' ≠ C'' ∧ B' ≠ C'"
      using ‹outH B' C' C''› outH_expand by presburger
    hence "ColH B' C' C''" 
      by simp
    moreover have "B' ≠ C''" 
      using ‹ColH B' C' C'' ∧ B' ≠ C'' ∧ B' ≠ C'› by blast
    have "B' ≠ C'" 
      using ‹ColH B' C' C'' ∧ B' ≠ C'' ∧ B' ≠ C'› by blast
    moreover have "ColH B' D' D'' ∧ B' ≠ D'' ∧ B' ≠ D'" 
      using ‹outH B' D' D''› outH_expand by blast
    hence "ColH B' D' D''" 
      by simp
    moreover have "B' ≠ D''" 
      by (simp add: ‹ColH B' D' D'' ∧ B' ≠ D'' ∧ B' ≠ D'›)
    moreover have "B' ≠ D'" 
      using ‹ColH B' D' D'' ∧ B' ≠ D'' ∧ B' ≠ D'› by blast
    ultimately have "ColH A'' B' D''" 
      using ‹BetH A'' B' D''› between_col by blast
    hence "ColH A'' D'' B'" 
      using colH_permut_132 by blast
    have "A'' ≠ B'" 
      using ‹B' ≠ A''› by blast
    have "ColH A'' B' A'" 
      by (simp add: ‹ColH B' A' A''› colH_permut_312)
    have "ColH A'' B' B'" 
      by (simp add: colH_trivial122)
    have "A'' ≠ D''" 
      using ‹BetH A'' B' D''› not_betH121 by auto
    have "ColH A'' D'' A'" 
      using ‹A'' ≠ B'› ‹ColH A'' B' A'› ‹ColH A'' B' D''› 
        colH_trans colH_trivial121 by presburger
    moreover have "ColH A'' D'' B'" 
      by (simp add: ‹ColH A'' D'' B'›)
    moreover have "ColH A'' D'' C'"
    proof -
      have "ColH A'' C' D''" 
        by (metis ‹ColH A'' C'' D''› ‹ColH B' C' C'' ∧ B' ≠ C'' ∧ B' ≠ C'› calculation(2) 
            colH_permut_213 colH_trans colH_trivial121)
      thus ?thesis
        using colH_permut_132 by blast
    qed
    ultimately have "ColH A' B' C'" 
      using ‹A'' ≠ D''› colH_trans by blast
    hence False 
      by (simp add: assms(2))
  }
  have "CongaH A C D A'' C'' D'' ∧ CongaH A D C A'' D'' C'' ∧ CongH C D C'' D''"
  proof (rule th12)
    show "¬ ColH A C D" 
      using ‹ColH A C D ⟹ False› by auto
    show "¬ ColH A'' C'' D''" 
      using ‹ColH A'' C'' D'' ⟹ False› by auto
    show "CongH A C A'' C''" 
      using ‹CongaH B A C B' A'' C'' ∧ CongaH B C A B' C'' A'' ∧ CongH A C A'' C''› by blast
    show "CongH A D A'' D''" 
      by (simp add: ‹CongH A D A'' D''›)
    have "CongaH C A B C'' A'' B'" 
      using ‹CongaH B A C B' A'' C'' ∧ CongaH B C A B' C'' A'' ∧ CongH A C A'' C''› 
        conga_permlr by presburger
    moreover have "outH A C C" 
      by (metis assms(1) colH_trivial121 outH_trivial)
    moreover have "outH A'' C'' C''" 
      by (metis ‹¬ ColH A'' C'' D''› colH_trivial112 outH_trivial)
    moreover have "outH A B D" 
      by (simp add: assms(4) outH_def)
    moreover have "outH A'' B' D''" 
      using ‹BetH A'' B' D''› outH_def by auto
    ultimately show "CongaH C A D C'' A'' D''" 
      using conga_out_conga by blast
  qed
  have "¬ ColH D B C" 
    using assms(1) assms(4) betH_colH between_comm colH_trans colH_trivial122 by blast
  moreover have "¬ ColH D'' B' C''" 
    using ‹BetH A'' B' D''› ‹ColH A'' C'' D'' ⟹ False› betH_colH between_comm 
      colH_trans colH_trivial121 by blast
  moreover have "CongH D B D'' B'" 
    by (metis betH_distincts outH_expand ‹CongH B' D'' B D› 
        ‹outH B' D' D''› assms(4) congH_perms)
  moreover have "CongH D C D'' C''" 
    by (metis ‹CongaH A C D A'' C'' D'' ∧ CongaH A D C A'' D'' C'' ∧ CongH C D C'' D''› 
        calculation(2) colH_trivial121 congH_permlr)
  moreover have "CongaH B D C B' D'' C''"
  proof -
    have "CongaH A D C A'' D'' C''" 
      using ‹CongaH A C D A'' C'' D'' ∧ CongaH A D C A'' D'' C'' ∧ CongH C D C'' D''› by auto
    moreover have "outH D A B" 
      using assms(4) between_comm outH_def by blast
    moreover have "outH D C C" 
      by (metis ‹¬ ColH D B C› colH_trivial121 outH_trivial)
    moreover have "outH D'' A'' B'" 
      using between_comm ‹BetH A'' B' D''› outH_def by blast
    moreover have "outH D'' C'' C''" 
      by (metis ‹¬ ColH D'' B' C''› colH_trivial121 outH_trivial)
    ultimately show ?thesis
      using conga_out_conga by blast
  qed
  ultimately have "CongaH D B C D'' B' C''" 
    using th12 by blast
  have "CongaH D B C D' B' C'"
  proof -
    have "outH B D D" 
      using assms(4) betH_distincts outH_trivial by blast
    moreover have "outH B C C" 
      by (metis ‹¬ ColH A C D› assms(4) between_col outH_trivial)
    moreover have "outH B' D'' D'" 
      using ‹BetH A'' B' D''› ‹outH B' D' D''› betH_distincts outH_sym by presburger
    moreover have "outH B' C'' C'" 
      using ‹outH B' C' C''› outH_sym out_distinct by blast
    ultimately show ?thesis 
      using ‹CongaH D B C D'' B' C''› conga_out_conga by blast
  qed
  thus ?thesis 
    using conga_permlr by blast
qed

lemma congH_colH_betH:
  assumes "A ≠ B" and
    "A ≠ I" and
    "B ≠ I" and
    "CongH I A I B" and
    "ColH I A B"
  shows "BetH A I B"
proof -
  have "BetH I A B ⟶ ?thesis" 
    using assms(4) betH_not_congH by blast
  moreover have "BetH A B I ⟶ ?thesis" 
    by (metis assms(2) assms(4) betH_not_congH between_comm congH_sym)
  ultimately show ?thesis
    by (metis assms(1) assms(2) assms(3) assms(5) between_one)
qed

lemma plane_separation:
  assumes "¬ ColH A X Y" and
    "¬ ColH B X Y" and
    "IncidP A p" and
    "IncidP B p" and 
    "IncidP X p" and 
    "IncidP Y p"
  shows "cut' A B X Y ∨ same_side' A B X Y" 
proof -
  obtain l where "IsL l" and "IncidL X l" and "IncidL Y l" 
    using ColH_def colH_trivial122 by blast
  obtain C where "cut l A C" 
    using ColH_def ‹IncidL X l› ‹IncidL Y l› ‹IsL l› assms(1) cut_exists by blast
  have "A = B ⟶ ?thesis" 
    using assms(2) colH_permut_312 same_side_prime_refl by blast
  moreover {
    assume "A ≠ B" 
    have "A ≠ C" 
      using ‹local.cut l A C› cut_distinct by auto
    {
      assume "B = C"
      obtain m where "IncidL X m ∧ IncidL Y m" 
        using ‹IncidL X l› ‹IncidL Y l› by auto
      obtain I where "IncidL I l" and "BetH A I C"
        using ‹local.cut l A C› local.cut_def by blast
      have "¬ IncidL A l" 
        using ‹local.cut l A C› local.cut_def by auto
      have "¬ IncidL C l" 
        using ‹local.cut l A C› local.cut_def by blast
      have "cut l A C" 
        by (simp add: ‹local.cut l A C›)
      hence "cut l A B" 
        by (simp add: ‹B = C›)
      have "X ≠ Y" 
        using assms(1) colH_trivial122 by blast
      moreover
      {
        fix k
        assume "IsL k" and "IncidL X k" and "IncidL Y k"
        hence "cut k A B"  
          by (metis inter_incid_uniquenessH ‹B = C› ‹BetH A I C› ‹IncidL I l›
              ‹IncidL X k› ‹IncidL X l› ‹IncidL Y k› ‹IncidL Y l› ‹IsL k› ‹¬ IncidL A l›
              ‹¬ IncidL C l› calculation local.cut_def)
      }
      ultimately have "cut' A B X Y"
        using cut'_def by presburger
      hence ?thesis
        by blast
    }
    moreover 
    {
      assume "B ≠ C"
      hence ?thesis 
      proof (cases "ColH A C B")
        case True
        hence "ColH A C B" 
          by simp
        obtain I where "IncidL I l" and "BetH A I C" 
          using ‹local.cut l A C› local.cut_def by blast
        hence "ColH A I C" 
          using between_col by blast
        have "ColH A I B" 
          by (meson True ‹A ≠ C› ‹ColH A I C› colH_permut_132 colH_trans colH_trivial121)
        have "¬ IncidL A l" 
          using ‹local.cut l A C› local.cut_def by auto
        {
          assume "BetH A I B"
          {
            fix m
            assume "IsL m" and "IncidL X m" and "IncidL Y m"
            hence "EqL m l" 
              by (metis ‹IncidL X l› ‹IncidL Y l› ‹IsL l› assms(2) 
                  colH_trivial122 line_uniqueness)
            hence "cut m A B" 
              using ColH_def ‹BetH A I B› ‹IncidL I l› ‹IncidL X m› ‹IncidL Y m› 
                ‹IsL l› ‹IsL m› ‹¬ IncidL A l› assms(2) local.cut_def morph by auto
          }
          hence  "cut' A B X Y" 
            using assms(1) colH_trivial122 cut'_def by auto
          hence ?thesis
            by blast
        }
        moreover {
          assume "BetH I B A"
          {
            fix m
            assume "IsL m" and "IncidL X m" and "IncidL Y m"
            hence "EqL m l" 
              by (metis ‹IncidL X l› ‹IncidL Y l› ‹IsL l› assms(2) 
                  colH_trivial122 line_uniqueness)
            hence "same_side A B m" 
              by (metis inter_incid_uniquenessH ncolH_distincts out_same_side 
                  outH_def ‹BetH I B A› ‹IncidL I l› ‹IncidL X l› ‹IncidL X m› ‹IncidL Y l›
                  ‹IncidL Y m› ‹¬ IncidL A l› assms(2))
          }
          hence "same_side' A B X Y" 
            using assms(1) colH_trivial122 same_side'_def by auto
          hence ?thesis
            by blast
        }
        moreover {
          assume "BetH I A B"
          {
            fix m
            assume "IsL m" and "IncidL X m" and "IncidL Y m"
            hence "EqL m l" 
              by (metis ‹IncidL X l› ‹IncidL Y l› ‹IsL l› assms(2) 
                  colH_trivial122 line_uniqueness)
            hence "same_side A B m" 
              by (metis inter_incid_uniquenessH ncolH_expand out_same_side 
                  outH_def ‹BetH I A B› ‹IncidL I l› ‹IncidL X l› ‹IncidL X m› ‹IncidL Y l›
                  ‹IncidL Y m› ‹¬ IncidL A l› assms(2))
          }
          hence "same_side' A B X Y" 
            using assms(1) colH_trivial122 same_side'_def by auto
          hence ?thesis
            by blast
        }
        ultimately show ?thesis 
          by (metis ColH_def Is_line ‹A ≠ B› ‹BetH A I C› ‹ColH A I B›
              ‹IncidL I l› ‹IncidL X l› ‹IncidL Y l› assms(2) betH_colH between_one)
      next
        case False
        have "IncidLP l p" 
          using ncolH_expand Is_plane ‹IncidL X l› ‹IncidL Y l› ‹IsL l›
            assms(2) assms(5) assms(6) line_on_plane by blast
        obtain I where "IncidL I l" and "BetH A I C" 
          using ‹local.cut l A C› local.cut_def by blast
        hence "ColH A I C" 
          by (simp add: between_col)
        hence "IncidP I p" 
          using IncidLP_def ‹IncidL I l› ‹IncidLP l p› by blast
        hence "IncidP C p" 
          using ‹BetH A I C› ‹ColH A I C› assms(3) betH_distincts line_on_plane' by blast
        {
          assume "cut l A B"
          {
            fix m
            assume "IsL m" and "IncidL X m" and "IncidL Y m"
            hence "EqL m l" 
              by (metis ‹IncidL X l› ‹IncidL Y l› ‹IsL l› assms(2) 
                  colH_trivial122 line_uniqueness)
            hence "cut m A B" 
              by (meson ‹IsL m› ‹local.cut l A B› local.cut_def morph)
          }
          hence ?thesis 
            using assms(1) colH_trivial122 cut'_def by force
        }
        moreover
        {
          assume "cut l C B"
          have "X ≠ Y" 
            using assms(1) colH_trivial122 by blast
          {
            fix m
            assume "IsL m" and "IncidL X m" and "IncidL Y m"
            hence "EqL m l" 
              by (metis ‹IncidL X l› ‹IncidL Y l› ‹IsL l› assms(2) 
                  colH_trivial122 line_uniqueness)
            have "cut m A C" 
              by (meson ‹EqL m l› ‹IsL m› ‹local.cut l A C› local.cut_def morph)
            moreover have "cut m B C" 
              by (metis ‹EqL m l› ‹local.cut l C B› calculation cut_comm local.cut_def morph)
            ultimately have "same_side A B m" 
              using ‹IsL m› same_side_def by blast
          }
          hence "same_side' A B X Y" 
            using assms(1) colH_trivial122 same_side'_def by auto
          hence ?thesis 
            by blast
        }
        moreover 
        have "¬ IncidL B l" 
          using ColH_def ‹IncidL X l› ‹IncidL Y l› ‹IsL l› assms(2) by blast
        ultimately show ?thesis 
          using pasch False ‹IncidLP l p› ‹IncidP C p› ‹local.cut l A C› 
            assms(3) assms(4) strong_pasch by blast
      qed
    }
    ultimately have ?thesis 
      by blast
  }
  ultimately show ?thesis 
    by blast
qed

lemma same_side_comm:
  assumes "same_side A B l"
  shows "same_side B A l" 
  using assms same_side_def by blast

lemma same_side_not_incid:
  assumes "same_side A B l" 
  shows "¬ IncidL A l ∧ ¬ IncidL B l" 
  using assms local.cut_def same_side_def by auto

lemma out_same_side':
  assumes "X ≠ Y" and
    "IncidL X l" and 
    "IncidL Y l" and
    "IncidL A l" and
    "¬ IncidL B l" and
    "outH A B C"
  shows "same_side' B C X Y"
proof -
  have "same_side B C l" 
    using assms(4) assms(5) assms(6) out_same_side by blast
  {
    fix m
    assume "IsL m" and
      "IncidL X m" and
      "IncidL Y m"
    hence "EqL m l" 
      using Is_line assms(1) assms(2) assms(3) line_uniqueness by presburger
    hence "same_side B C m" 
      by (meson Is_line ‹IsL m› assms(4) assms(5) assms(6) morph out_same_side)
  }
  thus ?thesis
    by (simp add: assms(1) same_side'_def)
qed

lemma same_side_trans:
  assumes "same_side A B l" and
    "same_side B C l"
  shows "same_side A C l" 
  by (meson assms(1) assms(2) cut_comm cut_same_side_cut same_side_def)

lemma colH_IncidL__IncidL:
  assumes "A ≠ B" and
    "IncidL A l" and
    "IncidL B l" and
    "ColH A B C" 
  shows "IncidL C l" 
  using ColH_def assms(1) assms(2) assms(3) assms(4) inter_incid_uniquenessH by blast

lemma IncidL_not_IncidL__not_colH:
  assumes "A ≠ B" and
    "IncidL A l" and
    "IncidL B l" and
    "¬ IncidL C l"
  shows "¬ ColH A B C" 
  using assms(1) assms(2) assms(3) assms(4) colH_IncidL__IncidL by blast

lemma same_side_prime_not_colH:
  assumes "same_side' A B C D" 
  shows "¬ ColH A C D ∧ ¬ ColH B C D" 
proof -
  {
    fix l 
    assume "IncidL C l" and
      "IncidL D l"
    have "same_side A B l" 
      using Is_line ‹IncidL C l› ‹IncidL D l› assms same_side'_def by auto
    hence ?thesis 
      by (meson ColH_def assms same_side'_def same_side_not_incid)
  }
  thus ?thesis 
    by (metis assms line_existence same_side'_def)
qed

lemma OS2__TS:
  assumes "same_side' Y Z PO X" and
    "same_side' X Y PO Z"
  shows "cut' X Z PO Y" 
proof -
  obtain Z' where "BetH Z PO Z'" 
    using assms(2) between_out same_side'_def by force
  have "PO ≠ X" 
    using assms(1) same_side'_def by blast
  have "PO ≠ Z" 
    using assms(2) same_side'_def by force
  {
    fix l 
    assume "IsL l" and
      "IncidL PO l" and
      "IncidL X l"
    have "¬ IncidL Y l" 
      using ColH_def ‹IncidL PO l› ‹IncidL X l› ‹IsL l› assms(1) 
        same_side_prime_not_colH by blast
    moreover have "¬ IncidL Z l" 
      using ColH_def ‹IncidL PO l› ‹IncidL X l› ‹IsL l› assms(1) 
        same_side_prime_not_colH by blast
    ultimately have "cut l Z' Z" 
      by (metis IncidL_not_IncidL__not_colH Is_line ‹BetH Z PO Z'› ‹IncidL PO l› 
          betH_distincts between_col between_comm local.cut_def)
    hence "cut l Y Z'" 
      by (meson ‹IncidL PO l› ‹IncidL X l› ‹IsL l› assms(1) cut_comm 
          cut_same_side_cut same_side'_def same_side_comm)
  }
  hence "cut' Y Z' PO X" 
    using ‹PO ≠ X› cut'_def by auto
  {
    fix l
    assume "IsL l" and
      "IncidL PO l" and
      "IncidL Y l"
    have "¬ ColH Y PO Z" 
      using assms(2) same_side_prime_not_colH by blast
    have "PO ≠ Y" 
      using ‹¬ ColH Y PO Z› colH_trivial112 by auto
    have "PO ≠ Z'" 
      using ‹BetH Z PO Z'› betH_distincts by auto
    have "Z ≠ Z'" 
      using ‹BetH Z PO Z'› not_betH121 by auto
    {
      assume "IncidL Z' l" 
      hence "ColH PO Y Z'" 
        using ColH_def ‹IncidL PO l› ‹IncidL Y l› ‹IsL l› by blast
      moreover have "ColH Z PO Z'" 
        by (simp add: ‹BetH Z PO Z'› betH_colH)
      ultimately have "ColH Y PO Z" 
        by (meson ColH_def ‹PO ≠ Z'› inter_incid_uniquenessH)
      have False 
        using ColH_def ‹BetH Z PO Z'› ‹IncidL PO l› ‹IncidL Y l› 
          ‹IncidL Z' l› ‹IsL l› ‹PO ≠ Z'› ‹¬ ColH Y PO Z› betH_line 
          inter_incid_uniquenessH by blast
    }
    hence "cut l Z Z'" 
      using ColH_def ‹BetH Z PO Z'› ‹IncidL PO l› ‹IncidL Y l› 
        ‹IsL l› ‹¬ ColH Y PO Z› local.cut_def by blast
    moreover
    obtain m where "IsL m" and "IncidL PO m" and "IncidL X m"
      using ‹PO ≠ X› line_existence by blast
    have "cut m Y Z'" 
      using Is_line ‹IncidL PO m› 
        ‹IncidL X m› ‹⋀l. ⟦IsL l; IncidL PO l; IncidL X l⟧ ⟹ local.cut l Y Z'› by blast
    have "¬ IncidL Y m" 
      using ‹local.cut m Y Z'› local.cut_def by blast
    have "¬ IncidL Z' m" 
      using ‹local.cut m Y Z'› local.cut_def by auto
    obtain X' where "IncidL X' m" and "BetH Y X' Z'" 
      using ‹local.cut m Y Z'› local.cut_def by blast
    have "same_side Z' X' l" 
      using ‹BetH Y X' Z'› ‹IncidL Y l› ‹IncidL Z' l ⟹ False› outH_def out_same_side by blast
    moreover have "same_side X' X l" 
    proof -
      have "ColH PO X X'" 
        using ColH_def Is_line ‹IncidL PO m› ‹IncidL X m› ‹IncidL X' m› by blast
      have "¬ ColH Y PO X" 
        using assms(1) same_side_prime_not_colH by presburger
      have "outH PO X X'" 
      proof (cases "X = X'")
        case True
        thus ?thesis 
          using ‹PO ≠ X› outH_trivial by auto
      next
        case False
        hence "X ≠ X'" 
          by simp
        have "ColH Z PO Z'" 
          by (simp add: ‹BetH Z PO Z'› betH_colH)
        have "ColH Y X' Z'" 
          by (simp add: ‹BetH Y X' Z'› betH_colH)
        have "PO = X' ⟶ ?thesis" 
          using ‹IncidL PO l› calculation(2) same_side_not_incid by blast
        moreover
        {
          assume "PO ≠ X'"
          have "ColH PO X X'" 
            by (simp add: ‹ColH PO X X'›)
          hence "BetH PO X X' ∨ BetH X X' PO ∨ BetH X PO X'" 
            using False ‹PO ≠ X'› ‹PO ≠ X› between_one by auto
          moreover have "BetH PO X X' ⟶ ?thesis" 
            using outH_def by auto
          moreover have "BetH X X' PO ⟶ ?thesis" 
            using between_comm outH_def by blast
          moreover {
            assume "BetH X PO X'"
            obtain lo where "IsL lo" and "IncidL PO lo" and "IncidL Z lo" 
              using ‹PO ≠ Z› line_existence by blast
            have "same_side X Y lo" 
              using ‹IncidL PO lo› ‹IncidL Z lo› ‹IsL lo› assms(2) same_side'_def by auto
            have "cut lo X X'" 
              by (metis Is_line ‹BetH X PO X'› ‹ColH PO X X'› ‹IncidL PO lo› 
                  ‹PO ≠ X'› ‹same_side X Y lo› colH_IncidL__IncidL colH_permut_312 
                  local.cut_def same_side_not_incid)
            moreover
            have "¬ IncidL X' lo" 
              using calculation local.cut_def by blast
            moreover have "IncidL Z' lo" 
              by (metis ‹ColH Z PO Z'› ‹IncidL PO lo› ‹IncidL Z lo›
                  ‹PO ≠ Z› colH_IncidL__IncidL)
            ultimately have "same_side X' Y lo" 
              by (meson ‹BetH Y X' Z'› between_comm outH_def out_same_side)
            hence ?thesis 
              using ‹local.cut lo X X'› ‹same_side X Y lo› cut_same_side_cut 
                same_side_not_cut by blast
          }
          ultimately have ?thesis 
            by blast
        }
        ultimately show ?thesis 
          by blast
      qed
      thus ?thesis 
        by (meson ‹IncidL PO l› ‹IncidL PO m› ‹IncidL X m› ‹IncidL Y l› 
            ‹PO ≠ X› ‹¬ IncidL Y m› inter_incid_uniquenessH out_same_side same_side_comm)
    qed    
    ultimately have "same_side Z' X l" 
      using same_side_trans by blast
    hence "cut l X Z" 
      using ‹local.cut l Z Z'› cut_comm cut_same_side_cut by blast
  }
  thus ?thesis 
    by (metis assms(2) colH_trivial112 cut'_def same_side_prime_not_colH)
qed

lemma th15_aux_1:
  assumes "¬ ColH H PO L" and
    "¬ ColH H' O' L'" and
    "¬ ColH K PO L" and
    "¬ ColH K' O' L'" and
    "¬ ColH H PO K" and
    "¬ ColH H' O' K'" and
    "same_side' H K PO L" and
    "same_side' H' K' O' L'" and
    "cut' K L PO H" and
    "CongaH H PO L H' O' L'" and
    "CongaH K PO L K' O' L'"
  shows "CongaH H PO K H' O' K'" 
proof -
  obtain K'' where "CongH O' K'' PO K" and "outH O' K' K''" 
    by (metis assms(3) assms(4) colH_trivial112 out_construction)
  obtain L'' where "CongH O' L'' PO L" and "outH O' L' L''" 
    by (metis assms(3) assms(4) colH_trivial122 out_construction)
  have "CongaH K PO L K'' O' L''" 
    using ‹outH O' K' K''› ‹outH O' L' L''› assms(1) assms(11) assms(5) 
      conga_out_conga ncolH_distincts outH_trivial by blast
  have "PO ≠ H" 
    using assms(1) colH_trivial112 by blast
  obtain l where "IsL l" and "IncidL PO l" and "IncidL H l" 
    using ‹PO ≠ H› line_existence by fastforce
  hence "cut l K L" 
    using assms(9) cut'_def by auto
  have "¬ IncidL K l" 
    using ‹local.cut l K L› local.cut_def by blast
  have "¬ IncidL L l" 
    using ‹local.cut l K L› local.cut_def by auto
  obtain I where "IncidL I l" and "BetH K I L" 
    using ‹local.cut l K L› local.cut_def by blast
  have "PO ≠ I" 
    using ‹BetH K I L› assms(3) betH_colH by blast
  have "H = I ⟶ outH PO I H" 
    using ‹PO ≠ I› outH_trivial by force
  moreover {
    assume "H ≠ I"
    have "ColH PO I H" 
      using ColH_def Is_line ‹IncidL H l› ‹IncidL I l› ‹IncidL PO l› by blast
    hence "BetH PO I H ∨ BetH I H PO ∨ BetH I PO H" 
      using between_one ‹H ≠ I› ‹PO ≠ H› ‹PO ≠ I› by blast
    moreover have "BetH PO I H ⟶ outH PO I H" 
      by (simp add: outH_def)
    moreover have "BetH I H PO ⟶ outH PO I H" 
      using between_comm outH_def by blast
    moreover {
      assume "BetH I PO H"
      have "PO ≠ L" 
        using ‹IncidL PO l› ‹¬ IncidL L l› by auto
      obtain m where "IsL m" and "IncidL PO m" and "IncidL L m" 
        using ColH_def colH_trivial121 by blast
      have "same_side H K m" 
        using ‹IncidL L m› ‹IncidL PO m› ‹IsL m› assms(7) same_side'_def by auto
      have "cut m H I" 
        by (metis IncidL_not_IncidL__not_colH Is_line ‹BetH I PO H› ‹ColH PO I H› 
            ‹IncidL PO m› ‹PO ≠ I› ‹same_side H K m› 
            cut_comm local.cut_def same_side_not_incid)
      moreover have "same_side I K m" 
        by (meson ‹BetH K I L› ‹IncidL L m› between_comm calculation local.cut_def 
            outH_def out_same_side)
      ultimately have "cut m H K" 
        using cut_same_side_cut by blast
      hence "outH PO I H" 
        using ‹same_side H K m› same_side_not_cut by auto
    }
    ultimately have "outH PO I H" 
      by blast
  }
  ultimately have "outH PO I H"
    by blast
  have "outH PO L L" 
    using assms(7) outH_trivial same_side'_def by force
  obtain I' where "CongH O' I' PO I" and "outH O' H' I'" 
    by (metis ‹PO ≠ I› assms(2) colH_trivial112 out_construction)
  hence "CongaH I PO L I' O' L''" 
    using ‹PO ≠ H› ‹outH O' L' L''› ‹outH PO I H› ‹outH PO L L› assms(10) 
      conga_out_conga outH_sym by blast
  have "O' ≠ I'" 
    using ‹outH O' H' I'› out_distinct by auto
  have "I' ≠ L''" 
    by (metis (mono_tags, opaque_lifting) ‹O' ≠ I'› ‹outH O' H' I'› ‹outH O' L' L''› 
        assms(2) colH_trans ncolH_expand outH_col)
  hence "∃ I'. (O' ≠ I' ∧ I' ≠ L'' ∧ outH PO H I ∧ outH O' H' I' ∧
              ColH O' I' H' ∧ CongH O' I' PO I ∧ CongaH I PO L I' O' L'')" 
    using ‹CongH O' I' PO I› ‹CongaH I PO L I' O' L''› ‹O' ≠ I'› ‹PO ≠ H›
      ‹outH O' H' I'› ‹outH PO I H› outH_col outH_sym by blast
  then obtain I' where "O' ≠ I'" and "I' ≠ L''" and 
    "outH PO H I" and "outH O' H' I'" and
    "ColH O' I' H'" and "CongH O' I' PO I" and "CongaH I PO L I' O' L''" 
    by blast
  have "PO ≠ L" 
    using ‹IncidL PO l› ‹¬ IncidL L l› by blast
  have "O' ≠ L''" 
    using ‹outH O' L' L''› out_distinct by blast
  have "ColH O' L' L''" 
    using ‹outH O' L' L''› outH_expand by blast
  have "CongaH PO I L O' I' L'' ∧ CongaH PO L I O' L'' I' ∧ CongH I L I' L''"
  proof -
    have "¬ ColH PO I L" 
      using ‹IncidL I l› ‹IncidL PO l› ‹PO ≠ I› ‹¬ IncidL L l›
        colH_IncidL__IncidL by blast
    moreover 
    {
      assume "ColH O' I' L''" 
      have False
        by (metis ‹ColH O' I' H'› ‹ColH O' I' L''› ‹ColH O' L' L''› ‹O' ≠ I'› ‹O' ≠ L''› 
            assms(2) colH_permut_312 inter_uniquenessH ncolH_expand)
    }
    hence "¬ ColH O' I' L''" 
      by blast
    moreover have "CongH PO I O' I'" 
      using ‹CongH O' I' PO I› ‹O' ≠ I'› congH_sym by blast
    moreover have "CongH PO L O' L''" 
      using ‹CongH O' L'' PO L› ‹O' ≠ L''› congH_sym by blast
    moreover have "CongaH I PO L I' O' L''" 
      by (simp add: ‹CongaH I PO L I' O' L''›)
    ultimately show ?thesis
      using th12 by blast
  qed
  have "CongaH PO I L O' I' L''" 
    using ‹CongaH PO I L O' I' L'' ∧ CongaH PO L I O' L'' I' ∧ CongH I L I' L''› by auto
  have "CongaH PO L I O' L'' I'" 
    using ‹CongaH PO I L O' I' L'' ∧ CongaH PO L I O' L'' I' ∧ CongH I L I' L''› by auto
  have "CongH I L I' L''" 
    using ‹CongaH PO I L O' I' L'' ∧ CongaH PO L I O' L'' I' ∧ CongH I L I' L''› by blast
  have "PO ≠ K" 
    using ‹IncidL PO l› ‹¬ IncidL K l› by auto
  have "PO ≠ L" 
    by (simp add: ‹PO ≠ L›)
  have "ColH O' L' L''" 
    using ‹ColH O' L' L''› by blast
  have "O' ≠ L'" 
    using ‹outH O' L' L''› outH_expand by presburger
  have "CongaH PO K L O' K'' L'' ∧ CongaH PO L K O' L'' K'' ∧ CongH K L K'' L''" 
  proof -
    have "¬ ColH PO K L" 
      using assms(3) colH_permut_213 by blast
    moreover 
    {
      assume "ColH O' K'' L''"
      have "O' ≠ K''" 
        using ‹outH O' K' K''› out_distinct by presburger
      have "K'' ≠ L''" 
        by (metis ‹ColH O' L' L''› ‹outH O' K' K''› assms(4) colH_trans 
            ncolH_expand outH_expand) 
      have "O' ≠ K'" 
        using assms(6) colH_trivial122 by blast
      have "K' ≠ L'" 
        using assms(4) ncolH_expand by presburger
      have "ColH O' K' L'"
        by (metis ‹ColH O' K'' L''› ‹ColH O' L' L''› ‹O' ≠ K''› ‹O' ≠ L''› 
            ‹outH O' K' K''› colH_trans ncolH_expand outH_col)
      have False 
        using ‹ColH O' K' L'› assms(4) colH_permut_213 by blast
    }
    hence "¬ ColH O' K'' L''"
      by blast
    moreover have "CongH PO K O' K''" 
      using ‹CongH O' K'' PO K› ‹outH O' K' K''› congH_sym out_distinct by presburger
    moreover have "CongH PO L O' L''" 
      using ‹CongH O' L'' PO L› ‹O' ≠ L''› congH_sym by presburger
    moreover have "CongaH K PO L K'' O' L''" 
      by (simp add: ‹CongaH K PO L K'' O' L''›)
    ultimately show ?thesis 
      using th12 by blast
  qed
  have "CongaH PO K L O' K'' L''" 
    using ‹CongaH PO K L O' K'' L'' ∧ CongaH PO L K O' L'' K'' ∧ CongH K L K'' L''› by auto
  have "CongaH PO L K O' L'' K''" 
    using ‹CongaH PO K L O' K'' L'' ∧ CongaH PO L K O' L'' K'' ∧ CongH K L K'' L''› by auto
  have "CongH K L K'' L''" 
    using ‹CongaH PO K L O' K'' L'' ∧ CongaH PO L K O' L'' K'' ∧ CongH K L K'' L''› by auto
  have "BetH K'' I' L''" 
  proof -
    have "outH L PO PO" 
      using ‹PO ≠ L› outH_def by auto
    have "outH L'' O' O'" 
      using ‹O' ≠ L''› outH_def by auto
    have "outH L'' I' I'" 
      using ‹I' ≠ L''› outH_def by blast
    have "outH L I K" 
      using ‹BetH K I L› between_comm outH_def by blast
    hence "CongaH PO L K O' L'' I'" 
      using conga_out_conga ‹CongaH PO L I O' L'' I'› ‹outH L PO PO› ‹outH L'' I' I'›
        ‹outH L'' O' O'› by blast
    moreover 
    have "same_side' H' I' L'' O'" 
    proof -
      obtain m where "IsL m" and "IncidL O' m" and "IncidL L'' m" 
        using ‹O' ≠ L''› line_existence by blast
      have "L'' ≠ O'" 
        using ‹O' ≠ L''› by auto
      moreover have "IncidL L'' m" 
        by (simp add: ‹IncidL L'' m›)
      moreover have "IncidL O' m" 
        using ‹IncidL O' m› by auto
      moreover 
      {
        assume "IncidL H' m" 
        hence "ColH O' L'' H'" 
          using ColH_def ‹IsL m› calculation(2) calculation(3) by blast
        hence False 
          by (metis ‹ColH O' L' L''› assms(2) calculation(1) colH_trans ncolH_distincts)
      }
      hence "¬ IncidL H' m" 
        by blast
      moreover have "outH O' H' I'" 
        using ‹outH O' H' I'› by blast
      ultimately show ?thesis using out_same_side' 
        by blast
    qed
    moreover 
    have "L'' ≠ O'" 
      using ‹O' ≠ L''› by blast
    moreover 
    have "∀ l. (IsL l ∧ IncidL L'' l ∧ IncidL O' l) ⟶ same_side H' K'' l" 
    proof -
      {
        fix l
        assume "IsL l" and
          "IncidL L'' l" and "IncidL O' l"
        have "ColH O' L' L''" 
          by (simp add: ‹ColH O' L' L''›)
        obtain lo where "IncidL O' lo" and "IncidL L' lo" and 
          "IncidL L'' lo" and "IncidL O' lo" 
          by (metis ‹outH O' L' L''› betH_line line_existence outH_def)
        have "EqL l lo" 
          using Is_line ‹IncidL L'' l› ‹IncidL L'' lo› ‹IncidL O' l› ‹IncidL O' lo› 
            calculation(3) line_uniqueness by presburger
        hence "same_side K' K'' lo" 
          using ColH_def Is_line ‹IncidL L' lo› ‹IncidL O' lo› ‹outH O' K' K''› assms(4) 
            out_same_side by blast
        hence "same_side H' K' lo" 
          using Is_line ‹IncidL L' lo› ‹IncidL O' lo› assms(8) same_side'_def by force
        hence "same_side H' K'' l" using same_side_trans 
          by (metis (no_types, lifting) ColH_def ‹IncidL L' lo› ‹IncidL L'' l›
              ‹IncidL L'' lo› ‹IncidL O' l› ‹IncidL O' lo› ‹IsL l› ‹outH O' K' K''› assms(4) 
              assms(8) calculation(3) inter_incid_uniquenessH out_same_side same_side'_def)
      }
      thus ?thesis 
        by blast
    qed
    ultimately have "same_side' H' K'' L'' O'" 
      using same_side'_def by blast
    thus ?thesis 
      by (metis ‹BetH K I L›  ‹CongaH PO L K O' L'' I'› ‹same_side' H' I' L'' O'› assms(3) 
          ‹CongaH PO I L O' I' L'' ∧ CongaH PO L I O' L'' I' ∧ CongH I L I' L''› 
          ‹CongaH PO K L O' K'' L'' ∧ CongaH PO L K O' L'' K'' ∧ CongH K L K'' L''›
          betH_congH3_outH_betH between_comm colH_permut_312 congH_permlr 
          cong_4_uniqueness out_distinct same_side_prime_not_colH)
  qed
  have "CongaH K PO I K'' O' I' ∧ CongaH K I PO K'' I' O' ∧ CongH PO I O' I'" 
  proof -
    have "CongH I' K'' I K" 
    proof -
      have "BetH L'' I' K''"       
        using ‹BetH K'' I' L''› between_comm by blast
      moreover have "BetH L I K"       
        by (simp add: ‹BetH K I L› between_comm)
      moreover have "CongH L'' I' L I"       
        using ‹BetH K I L› ‹CongH I L I' L''› ‹I' ≠ L''› betH_distincts 
          congH_perms by blast
      moreover have "CongH L'' K'' L K"       
        by (metis ‹CongH K L K'' L''› assms(3) calculation(1) colH_trivial121 
            congH_perms not_betH121)

      ultimately show ?thesis
        using soustraction_betH by blast
    qed
    have "¬ ColH K PO I" 
      by (metis IncidL_not_IncidL__not_colH ‹IncidL I l› ‹IncidL PO l› ‹PO ≠ I› 
          ‹¬ IncidL K l› colH_permut_321)
    moreover 
    {
      assume "ColH K'' O' I'"
      have "O' ≠ K''" 
        using ‹outH O' K' K''› out_distinct by blast
      have "ColH O' K' K''" 
        using ‹outH O' K' K''› outH_expand by auto
      hence "ColH K' O' L'" 
        by (metis colH_permut_231 colH_trans colH_trivial121 ‹ColH K'' O' I'› 
            ‹ColH O' I' H'› ‹O' ≠ I'› ‹O' ≠ K''› assms(6))
      hence False 
        by (simp add: assms(4))
    }
    hence "¬ ColH K'' O' I'" 
      by blast
    moreover have "CongH K PO K'' O'" 
      using outH_expand ‹CongH O' K'' PO K› ‹PO ≠ K› ‹outH O' K' K''› 
        congH_perms by blast
    moreover have "CongH K I K'' I'" 
      by (metis ‹CongH I' K'' I K› ‹IncidL I l› ‹¬ IncidL K l› calculation(2) 
          colH_trivial121 congH_perms)
    moreover have "CongaH PO K I O' K'' I'" 
      using ‹BetH K I L› ‹BetH K'' I' L''› ‹CongaH PO K L O' K'' L''› ‹PO ≠ K› 
        calculation(2) conga_out_conga ncolH_expand outH_def by blast
    ultimately 
    show ?thesis using th12 by blast
  qed
  have "CongaH K PO I K'' O' I'" 
    using ‹CongaH K PO I K'' O' I' ∧ CongaH K I PO K'' I' O' ∧ CongH PO I O' I'› by blast
  have "CongaH K I PO K'' I' O'" 
    using ‹CongaH K PO I K'' O' I' ∧ CongaH K I PO K'' I' O' ∧ CongH PO I O' I'› by auto
  have "CongH PO I O' I'" 
    using ‹CongH O' I' PO I› ‹O' ≠ I'› congH_sym by auto
  have "outH PO K K"     
    using ‹PO ≠ K› outH_def by force
  moreover have "outH PO I H"     
    by (simp add: ‹outH PO I H›)
  moreover have "outH O' K'' K'"     
    using ‹outH O' K' K''› outH_sym out_distinct by blast
  moreover have "outH O' I' H'"     
    by (simp add: ‹O' ≠ I'› ‹outH O' H' I'› outH_sym)
  ultimately show ?thesis 
    using ‹CongaH K PO I K'' O' I'› conga_out_conga conga_permlr by blast
qed

lemma th15_aux:
  assumes "¬ ColH H PO L" and
    "¬ ColH H' O' L'" and
    "¬ ColH K PO L" and
    "¬ ColH K' O' L'" and
    "¬ ColH H PO K" and
    "¬ ColH H' O' K'" and
    "same_side' H K PO L" and
    "same_side' H' K' O' L'" and
    "CongaH H PO L H' O' L'" and
    "CongaH K PO L K' O' L'"
  shows "CongaH H PO K H' O' K'" 
proof -
  obtain p where "IsP p" and "IncidP H p" and "IncidP K p" and 
    "IncidP PO p" and "IncidP L p" 
    using Is_plane assms(7) same_side_prime__plane by blast
  moreover have "cut' K L PO H ⟶ CongaH H PO K H' O' K'" 
    using assms(1) assms(10) assms(2) assms(3) assms(4) assms(5) assms(6) 
      assms(7) assms(8) assms(9) th15_aux_1 by auto
  moreover {
    assume "same_side' K L PO H"
    moreover have "¬ ColH K PO H" 
      using assms(5) colH_permut_321 by blast
    moreover have "¬ ColH K' O' H'" 
      using assms(6) colH_permut_321 by blast
    moreover
    have "PO ≠ L" 
      using assms(3) colH_trivial122 by blast
    {
      fix l
      assume "IsL l" and "IncidL PO l" and "IncidL L l"
      hence "same_side K H l" 
        by (metis assms(7) same_side'_def same_side_comm)
    }
    hence "same_side' K H PO L" 
      using ‹PO ≠ L› same_side'_def by auto
    moreover have "O' ≠ L'" 
      using assms(4) colH_trivial122 by force
    {
      fix l
      assume "IsL l" and "IncidL O' l" and "IncidL L' l"
      hence "same_side K' H' l" 
        by (meson assms(8) same_side'_def same_side_comm)
    }
    hence "same_side' K' H' O' L'" 
      by (simp add: ‹O' ≠ L'› same_side'_def)
    moreover have "cut' H L PO K" 
      by (simp add: OS2__TS assms(7) calculation(1))
    ultimately have "CongaH H PO K H' O' K'" 
      using assms(1) assms(2) assms(3) assms(4) assms(9) assms(10) 
        conga_permlr th15_aux_1 by presburger
  }
  moreover have "¬ ColH K PO H" 
    using assms(5) colH_permut_321 by blast
  moreover have "¬ ColH L PO H" 
    using assms(1) colH_permut_321 by blast
  ultimately show ?thesis 
    using plane_separation by blast
qed

lemma th15:
  assumes "¬ ColH H PO L" and
    "¬ ColH H' O' L'" and
    "¬ ColH K PO L" and
    "¬ ColH K' O' L'" and
    "¬ ColH H PO K" and
    "¬ ColH H' O' K'" and
    "(cut' H K PO L ∧ cut' H' K' O' L') ∨ (same_side' H K PO L ∧ same_side' H' K' O' L')" and
    "CongaH H PO L H' O' L'" and
    "CongaH K PO L K' O' L'"
  shows "CongaH H PO K H' O' K'" 
proof -
  {
    assume "same_side' H K PO L" and "same_side' H' K' O' L'"
    hence ?thesis using th15_aux 
      using assms(1) assms(2) assms(3) assms(4) assms(5) assms(6) 
        assms(8) assms(9) by presburger
  }
  moreover
  {
    assume "cut' H K PO L" and
      "cut' H' K' O' L'" 
    obtain SH where "BetH H PO SH" 
      by (metis assms(1) between_out colH_trivial112)
    obtain SH' where "BetH H' O' SH'" 
      by (metis assms(2) between_out colH_trivial112)
    have "CongaH SH PO L SH' O' L'" 
      using ‹BetH H PO SH› ‹BetH H' O' SH'› assms(1) assms(2) assms(8)
        conga_permlr th14 by blast
    have "H ≠ PO" 
      using assms(1) colH_trivial112 by force
    have "PO ≠ SH" 
      using ‹BetH H PO SH› betH_distincts by blast
    have "H ≠ SH" 
      using ‹BetH H PO SH› not_betH121 by auto
    have "H' ≠ O'" 
      using assms(6) colH_trivial112 by force
    have "H' ≠ SH'" 
      using ‹BetH H' O' SH'› not_betH121 by force
    have "O' ≠ SH'" 
      using ‹BetH H' O' SH'› betH_distincts by blast
    have "CongaH SH PO K SH' O' K'" 
    proof -
      have "ColH H PO SH" 
        by (simp add: ‹BetH H PO SH› betH_colH)
      have "ColH H' O' SH'" 
        by (simp add: ‹BetH H' O' SH'› betH_colH)
      moreover have "¬ ColH SH PO L" 
        by (metis ‹ColH H PO SH› ‹PO ≠ SH› assms(1) colH_trans ncolH_expand)
      moreover have "¬ ColH SH' O' L'" 
        by (metis ‹ColH H' O' SH'› ‹O' ≠ SH'› assms(2) colH_permut_321 
            colH_trans colH_trivial122)
      moreover have "¬ ColH SH PO K" 
        by (metis ‹ColH H PO SH› ‹PO ≠ SH› assms(5) colH_permut_321 
            colH_trans colH_trivial122)
      moreover have "¬ ColH SH' O' K'" 
        by (metis ‹ColH H' O' SH'› ‹O' ≠ SH'› assms(6) colH_permut_321 
            colH_trans colH_trivial122)
      moreover 
      {
        fix l
        assume "IsL l" and "IncidL PO l" and "IncidL L l"
        hence "cut l SH H" 
          by (meson ColH_def ‹BetH H PO SH› assms(1) between_comm 
              calculation(2) local.cut_def)
        moreover
        have "cut l H K" 
          using ‹cut' H K PO L› ‹IncidL L l› ‹IncidL PO l› ‹IsL l› cut'_def by auto
        hence "cut l K H" 
          using cut_comm by blast
        ultimately have "same_side SH K l"  
          using same_side_def ‹IsL l› by blast
      }
      moreover have "PO ≠ L" 
        using calculation(2) colH_trivial122 by blast
      ultimately have "same_side' SH K PO L" 
        using same_side'_def by presburger
      moreover 
      {
        fix l
        assume "IsL l" and "IncidL O' l" and "IncidL L' l"
        hence "cut l SH' H'" 
          by (meson ColH_def ‹BetH H' O' SH'› ‹¬ ColH SH' O' L'› 
              assms(2) between_comm local.cut_def)
        moreover
        have "cut l H' K'"
          using ‹cut' H' K' O' L'› ‹IncidL L' l› ‹IncidL O' l› ‹IsL l› cut'_def by auto 
        hence "cut l K' H'" 
          using cut_comm by blast
        ultimately have "same_side SH' K' l"  
          using same_side_def ‹IsL l› by blast
      }
      moreover have "O' ≠ L'" 
        using assms(2) colH_trivial122 by force
      ultimately have "same_side' SH' K' O' L'" 
        using same_side'_def by presburger
      thus ?thesis
        using th15_aux ‹CongaH SH PO L SH' O' L'› ‹¬ ColH SH PO K› 
          ‹¬ ColH SH' O' K'› assms(9) same_side_prime_not_colH
          ‹same_side' SH K PO L› by blast
    qed
    moreover have "¬ ColH SH PO K" 
      using ‹BetH H PO SH› assms(5) betH_colH between_comm colH_trans colH_trivial122 by blast
    moreover have "¬ ColH SH' O' K'" 
      using ‹BetH H' O' SH'› assms(6) betH_colH between_comm colH_trans colH_trivial122 by blast
    moreover have "BetH SH PO H" 
      by (simp add: ‹BetH H PO SH› between_comm)
    moreover have "BetH SH' O' H'" 
      by (simp add: ‹BetH H' O' SH'› between_comm)
    ultimately have ?thesis 
      using conga_permlr th14 by blast
  }
  ultimately show ?thesis
    using assms(7) by fastforce
qed

lemma th17:
  assumes "¬ ColH X Y Z1" and
    "¬ ColH X Y Z2" and
    "ColH X I Y" and
    "BetH Z1 I Z2" and
    "CongH X Z1 X Z2" and
    "CongH Y Z1 Y Z2"
  shows "CongaH X Y Z1 X Y Z2" 
proof (cases "ColH Y Z1 Z2")
  case True
  hence "ColH Y Z1 Z2"
    by simp
  show ?thesis 
  proof (cases "ColH X Z1 Z2")
    case True
    hence "ColH X Z1 Z2"
      by simp
    have "ColH Z1 I Z2" 
      by (simp add: assms(4) betH_colH)
    have "Z1 ≠ Z2" 
      using assms(4) not_betH121 by blast
    hence "ColH X Y Z2" 
      by (metis True ‹ColH Y Z1 Z2› colH_permut_312 colH_trivial122 inter_uniquenessH)
    thus ?thesis
      using assms(2) by auto
  next
    case False
    hence "¬ ColH X Z1 Z2"
      by simp
    have "CongaH X Z1 Z2 X Z2 Z1" 
      by (simp add: False assms(5) isosceles_congaH)
    have "¬ ColH Z1 Y X" 
      using assms(1) colH_permut_321 by blast
    moreover have "¬ ColH Z2 Y X" 
      using assms(2) colH_permut_321 by blast
    moreover have "CongH Z1 Y Z2 Y" 
      using assms(2) assms(6) congH_permlr ncolH_expand by blast
    moreover have "CongH Z1 X Z2 X" 
      using False assms(5) congH_permlr ncolH_distincts by presburger
    moreover 
    have "BetH Z1 Y Z2" 
      by (metis False True assms(1) assms(6) calculation(2) colH_trivial112 
          colH_trivial122 congH_colH_betH)
    have "CongaH X Z1 Y X Z2 Y" 
    proof -
      have "outH Z1 X X" 
        by (metis False colH_trivial112 outH_trivial)
      moreover have "outH Z1 Z2 Y" 
        by (simp add: ‹BetH Z1 Y Z2› outH_def)
      moreover have "outH Z2 X X" 
        by (metis False colH_trivial121 outH_trivial)
      moreover have "outH Z2 Z1 Y" 
        using ‹BetH Z1 Y Z2› between_comm outH_def by blast
      ultimately show ?thesis 
        using ‹CongaH X Z1 Z2 X Z2 Z1› conga_out_conga by blast
    qed
    hence "CongaH Y Z1 X Y Z2 X" 
      using conga_permlr by presburger
    ultimately have "CongaH Z1 Y X Z2 Y X" 
      using cong_5 by blast
    thus ?thesis 
      using conga_permlr by blast
  qed
next
  case False
  hence "¬ ColH Y Z1 Z2"
    by simp
  show ?thesis 
  proof (cases "ColH X Z1 Z2")
    case True
    hence "ColH X Z1 Z2"
      by simp
    have "CongaH Y Z1 Z2 Y Z2 Z1" 
      by (simp add: False assms(6) isosceles_congaH)
    have "CongaH Z1 Y X Z2 Y X" 
    proof -
      have "¬ ColH Z1 Y X" 
        using assms(1) colH_permut_321 by blast
      moreover have "¬ ColH Z2 Y X" 
        using assms(2) colH_permut_321 by blast
      moreover have "CongH Z1 Y Z2 Y" 
        by (metis False assms(6) colH_trivial121 congH_permlr)
      moreover have "CongH Z1 X Z2 X" 
        using assms(2) assms(5) congH_permlr ncolH_expand by presburger
      moreover 
      have "BetH Z1 X Z2" 
        by (metis False True assms(2) assms(5) calculation(1) 
            colH_trivial121 colH_trivial122 congH_colH_betH)
      have "CongaH Y Z1 X Y Z2 X" 
      proof -
        have "outH Z1 Y Y" 
          by (metis False colH_trivial112 outH_trivial)
        moreover have "outH Z1 Z2 X" 
          by (simp add: ‹BetH Z1 X Z2› outH_def)
        moreover have "outH Z2 Y Y" 
          using ‹¬ ColH Z2 Y X› ncolH_expand outH_trivial by blast
        moreover have "outH Z2 Z1 X" 
          using ‹BetH Z1 X Z2› between_comm outH_def by blast
        ultimately show ?thesis 
          using ‹CongaH Y Z1 Z2 Y Z2 Z1› conga_out_conga by blast
      qed
      ultimately show ?thesis 
        using cong_5 by blast
    qed
    thus ?thesis 
      using conga_permlr by blast
  next
    case False
    hence "¬ ColH X Z1 Z2"
      by simp
    have "CongaH X Z1 Z2 X Z2 Z1" 
      by (simp add: False assms(5) isosceles_congaH)
    have "CongaH Y Z1 Z2 Y Z2 Z1" 
      by (simp add: ‹¬ ColH Y Z1 Z2› assms(6) isosceles_congaH)
    have "CongaH X Z1 Y X Z2 Y" 
    proof -
      have "¬ ColH X Z1 Z2" 
        by (simp add: False)
      moreover have "¬ ColH X Z2 Z1" 
        using calculation colH_permut_132 by blast
      moreover have "¬ ColH Y Z1 Z2" 
        by (simp add: ‹¬ ColH Y Z1 Z2›)
      moreover have "¬ ColH Y Z2 Z1" 
        using calculation(3) colH_permut_132 by blast
      moreover have "¬ ColH X Z1 Y" 
        using assms(1) colH_permut_132 by blast
      moreover have "¬ ColH X Z2 Y" 
        using assms(2) colH_permut_132 by blast
      moreover 
      have "cut' X Y Z1 Z2 ∧ cut' X Y Z2 Z1 ∨ same_side' X Y Z1 Z2 ∧ same_side' X Y Z2 Z1"
      proof -
        obtain p where "IsP p" and "IncidP X p" and "IncidP Y p" and "IncidP Z1 p"
          using assms(1) plan_existence by blast
        hence "IncidP Z2 p" 
          by (metis betH_colH assms(2) assms(3) assms(4) colH_permut_312 
              line_on_plane' ncolH_distincts)
        thus ?thesis 
          by (metis False ‹IncidP X p› ‹IncidP Y p› ‹IncidP Z1 p› calculation(2) 
              calculation(3) calculation(4) plane_separation same_side'_def)
      qed
      ultimately show ?thesis 
        by (simp add: ‹CongaH Y Z1 Z2 Y Z2 Z1› ‹CongaH X Z1 Z2 X Z2 Z1› th15)
    qed
    have "CongaH Z1 Y X Z2 Y X" 
    proof -
      have "¬ ColH Z1 Y X" 
        using assms(1) colH_permut_321 by blast
      moreover have "¬ ColH Z2 Y X" 
        using assms(2) colH_permut_321 by blast
      moreover have "CongH Z1 Y Z2 Y" 
        by (metis ‹¬ ColH Y Z1 Z2› assms(6) colH_trivial121 congH_permlr)
      moreover have "CongH Z1 X Z2 X" 
        by (metis assms(5) calculation(2) colH_trivial121 congH_permlr)
      moreover have "CongaH Y Z1 X Y Z2 X" 
        using ‹CongaH X Z1 Y X Z2 Y› conga_permlr by blast
      ultimately show ?thesis 
        using cong_5 by blast
    qed
    thus ?thesis 
      using conga_permlr by blast
  qed
qed

lemma congaH_existence_congH:
  assumes "U ≠ V" and
    "¬ ColH P PO X" and
    "¬ ColH A B C" 
  shows "∃ Y. (CongaH A B C X PO Y ∧ same_side' P Y PO X ∧ CongH PO Y U V)" 
proof -
  have "A ≠ B" 
    using assms(3) colH_trivial112 by blast
  have "C ≠ B" 
    using assms(3) colH_trivial122 by blast
  have "PO ≠ X" 
    using assms(2) colH_trivial122 by blast
  {
    fix x
    assume "CongaH A B C X PO x" and
      "same_side' P x PO X" 
    obtain Yaux where "CongaH A B C X PO Yaux" and "same_side' P Yaux PO X" 
      using ‹CongaH A B C X PO x› ‹same_side' P x PO X› by blast
    hence "¬ ColH Yaux PO X" 
      using same_side_prime_not_colH by blast
    {
      assume "PO = Yaux"
      hence "ColH Yaux PO X" 
        by (simp add: colH_trivial112)
      hence False 
        by (simp add: ‹¬ ColH Yaux PO X›)
    }
    {
      fix Y
      assume "CongH PO Y U V" and "outH PO Yaux Y"
      have "CongaH A B C X PO Y" 
      proof -
        have "CongaH A B C X PO Yaux" 
          using ‹CongaH A B C X PO Yaux› by blast
        moreover have "outH B A A" 
          using ‹A ≠ B› outH_trivial by auto
        moreover have "outH B C C" 
          using ‹C ≠ B› outH_trivial by presburger
        moreover have "outH PO X X" 
          using ‹PO ≠ X› outH_trivial by blast
        moreover have "outH PO Yaux Y" 
          using ‹outH PO Yaux Y› by auto
        ultimately show ?thesis 
          using conga_out_conga by blast
      qed
      moreover have "same_side' P Y PO X" 
        using ColH_def ‹¬ ColH Yaux PO X› ‹outH PO Yaux Y› 
          ‹same_side' P Yaux PO X› out_same_side same_side'_def same_side_trans by fastforce
      ultimately have "∃ Y. CongaH A B C X PO Y ∧ same_side' P Y PO X ∧ CongH PO Y U V" 
        using ‹CongH PO Y U V› by auto
    }
    hence ?thesis 
      using ‹PO = Yaux ⟹ False› assms(1) out_construction by blast
  }
  thus ?thesis 
    using assms(2) assms(3) cong_4_existence by blast
qed

lemma th18_aux:
  assumes "¬ ColH A B C" and
    "¬ ColH A' B' C'" and
    "CongH A B A' B'" and
    "CongH A C A' C'" and
    "CongH B C B' C'"
  shows "CongaH B A C B' A' C'" 
proof -
  have "A ≠ B" 
    using assms(1) colH_trivial112 by blast
  moreover
  have "C' ≠ B'" 
    using assms(2) colH_trivial122 by blast
  have "A' ≠ C'" 
    using assms(2) colH_trivial121 by force
  {
    fix B0
    assume "CongaH C A B C' A' B0" and "same_side' B' B0 A' C'" and "CongH A' B0 A B" 
    {
      fix P 
      assume "BetH B' C' P"
      { 
        fix B''
        assume "CongaH C A B C' A' B''" and "same_side' P B'' A' C'" and "CongH A' B'' A B"
        have "¬ ColH A' C' B0" 
          using ‹same_side' B' B0 A' C'› colH_permut_312 same_side_prime_not_colH by blast
        have "¬ ColH A' C' B''" 
          using ‹same_side' P B'' A' C'› colH_permut_312 same_side_prime_not_colH by blast
        have "CongH B C B0 C'" 
          by (metis ‹CongH A' B0 A B› ‹CongaH C A B C' A' B0› 
              ‹same_side' B' B0 A' C'› assms(1) assms(4) colH_permut_213 colH_trivial112 
              congH_sym conga_permlr same_side_prime_not_colH th12)
        have "CongH B C B'' C'" 
          by (metis ‹CongH A' B'' A B› ‹CongaH C A B C' A' B''› ‹¬ ColH A' C' B''› 
              assms(1) assms(4) colH_permut_132 congH_sym cong_permr ncolH_distincts th12)
        have "A' ≠ B''" 
          using ‹¬ ColH A' C' B''› colH_trivial121 by blast
        have "A' ≠ B0" 
          using ‹¬ ColH A' C' B0› colH_trivial121 by fastforce
        have "CongH A' B'' A' B0" 
          by (meson ‹A' ≠ B''› ‹A' ≠ B0› ‹CongH A' B'' A B› ‹CongH A' B0 A B›
              congH_sym cong_pseudo_transitivity)
        have "CongH B'' C' B0 C'" 
          using ‹CongH B C B'' C'› ‹CongH B C B0 C'› cong_pseudo_transitivity by blast
        have "CongH B'' C' B' C'" 
          using ‹CongH B C B'' C'› assms(5) cong_pseudo_transitivity by blast
        obtain l where "IsL l" and "IncidL A' l" and "IncidL C' l" 
          using ‹A' ≠ C'› line_existence by blast
        have "cut l B' P" 
          by (meson ColH_def Is_line ‹BetH B' C' P› ‹IncidL A' l› ‹IncidL C' l›
              ‹same_side' P B'' A' C'› assms(2) local.cut_def same_side_prime_not_colH)
        have "cut l B' B''" 
          using ‹IncidL A' l› ‹IncidL C' l› ‹IsL l› ‹local.cut l B' P›
            ‹same_side' P B'' A' C'› cut_same_side_cut same_side'_def by blast
        have "¬ IncidL B' l" 
          using ‹local.cut l B' P› local.cut_def by blast
        moreover have "¬ IncidL B'' l" 
          using ‹local.cut l B' B''› local.cut_def by blast
        moreover have "∃ I. IncidL I l ∧ BetH B' I B''" 
          using ‹local.cut l B' B''› local.cut_def by auto
        ultimately obtain I' where "ColH A' I' C'" and "BetH B' I' B''" 
          using ColH_def Is_line ‹IncidL A' l› ‹IncidL C' l› by blast
        have "cut l B'' B0" 
          by (meson ‹IncidL A' l› ‹IncidL C' l› ‹IsL l› ‹local.cut l B' B''›
              ‹same_side' B' B0 A' C'› cut_comm cut_same_side_cut same_side'_def)
        then obtain I where "ColH A' I C' ∧ BetH B0 I B''" 
          by (meson ColH_def ‹IncidL A' l› ‹IncidL C' l› cut_comm local.cut_def)
        have "CongaH C' A' B'' C' A' B0" 
        proof -
          have "¬ ColH C' A' B''" 
            using ‹¬ ColH A' C' B''› colH_permut_213 by blast
          moreover have "¬ ColH C' A' B0" 
            using ‹¬ ColH A' C' B0› colH_permut_213 by blast
          moreover have "ColH C' I A'" 
            using ‹ColH A' I C' ∧ BetH B0 I B''› colH_permut_321 by presburger
          moreover have "BetH B'' I B0" 
            by (simp add: ‹ColH A' I C' ∧ BetH B0 I B''› between_comm)
          moreover have "CongH C' B'' C' B0" 
            by (metis ‹CongH B'' C' B0 C'› calculation(2) colH_trivial121 congH_permlr)
          ultimately show ?thesis 
            using th17 ‹CongH A' B'' A' B0› by blast
        qed
        moreover have "outH A' B0 B'" 
        proof -
          have "¬ ColH B' A' C'" 
            using assms(2) colH_permut_213 by blast
          moreover have "¬ ColH C' A' B''" 
            using ‹¬ ColH A' C' B''› colH_permut_213 by blast
          moreover have "CongaH C' A' B'' C' A' B'" 
          proof -
            have "¬ ColH C' A' B'"
              using ‹¬ ColH B' A' C'› colH_permut_321 by blast
            moreover have "CongH C' B'' C' B'"
              using ‹C' ≠ B'› ‹CongH B'' C' B' C'› congH_permlr by presburger 
            moreover have "CongH A' B'' A' B'"
              by (metis cong_pseudo_transitivity ‹A' ≠ B''› ‹CongH A' B'' A B› assms(3) congH_sym) 
            ultimately show ?thesis
              using th17 [of C' A' B'' B'] between_comm ‹BetH B' I' B''› ‹ColH A' I' C'› 
                colH_permut_321 ‹¬ ColH C' A' B''› by blast 
          qed
          moreover have "same_side' B' B' A' C'" 
            using calculation(1) colH_permut_312 same_side_prime_refl by blast
          ultimately show ?thesis 
            using  ‹CongaH C' A' B'' C' A' B0› ‹same_side' B' B0 A' C'› 
              cong_4_uniqueness by blast
        qed
        ultimately have "CongaH B A C B' A' C'" 
          by (metis ‹A ≠ B› ‹A' ≠ B0› ‹CongH A' B0 A B› ‹CongaH C A B C' A' B0› 
              ‹outH A' B0 B'› assms(3) betH_not_congH congH_perms cong_pseudo_transitivity conga_permlr outH_def)
      }
      moreover have "¬ ColH P A' C'" 
        by (metis betH_expand ‹BetH B' C' P› assms(2) colH_permut_312 
            colH_trans colH_trivial121)
      moreover have "¬ ColH C A B" 
        using assms(1) colH_permut_231 by blast
      ultimately have "CongaH B A C B' A' C'" 
        using ‹A ≠ B› congaH_existence_congH by force
    }
    hence "CongaH B A C B' A' C'" 
      using ‹C' ≠ B'›between_out by presburger
  }
  moreover have "¬ ColH B' A' C'" 
    using assms(2) colH_permut_213 by blast
  moreover have "¬ ColH C A B" 
    using assms(1) colH_permut_231 by blast
  ultimately show ?thesis 
    using congaH_existence_congH by blast
qed

lemma th19:
  assumes "¬ ColH PO A B" and
    "¬ ColH O1 A1 B1" and
    "¬ ColH O2 A2 B2" and
    "CongaH A PO B A1 O1 B1" and
    "CongaH A PO B A2 O2 B2" 
  shows "CongaH A1 O1 B1 A2 O2 B2" 
proof -
  have "PO ≠ A" 
    using assms(1) colH_trivial112 by blast
  have "PO ≠ B" 
    using assms(1) colH_trivial121 by blast
  have "O1 ≠ A1" 
    using assms(2) colH_trivial112 by blast
  have "O1 ≠ B1" 
    using assms(2) colH_trivial121 by blast
  have "O2 ≠ A2" 
    using assms(3) colH_trivial112 by force
  have "O2 ≠ B2" 
    using assms(3) colH_trivial121 by blast
  {
    fix A1'
    assume "CongH O1 A1' PO A" and "outH O1 A1 A1'"
    {
      fix A2'
      assume "CongH O2 A2' PO A" and "outH O2 A2 A2'"
      {
        fix B1'
        assume "CongH O1 B1' PO B" and "outH O1 B1 B1'"
        {
          fix B2'
          assume "CongH O2 B2' PO B" and "outH O2 B2 B2'"
          have "O1 ≠ A1'" 
            using ‹outH O1 A1 A1'› outH_expand by blast
          have "O2 ≠ A2'" 
            using ‹outH O2 A2 A2'› outH_expand by auto
          have "O1 ≠ B1'" 
            using ‹outH O1 B1 B1'› out_distinct by auto
          have "O2 ≠ B2'" 
            using ‹outH O2 B2 B2'› outH_expand by blast
          {
            assume "ColH O1 A1' B1'"
            have "ColH O1 A1 A1'" 
              by (simp add: ‹outH O1 A1 A1'› outH_expand)
            have "ColH O1 B1 B1'" 
              by (simp add: ‹outH O1 B1 B1'› outH_expand)
            hence "ColH O1 A1 B1" 
              by (metis colH_trivial121 ‹ColH O1 A1 A1'› ‹ColH O1 A1' B1'› 
                  ‹ColH O1 B1 B1'› ‹O1 ≠ A1'› ‹O1 ≠ B1'› colH_permut_231 inter_uniquenessH)
            hence False 
              using assms(2) by blast
          }
          have "ColH O2 A2 A2'" 
            using ‹outH O2 A2 A2'› outH_expand by blast
          have "ColH O2 B2 B2'" 
            by (simp add: ‹outH O2 B2 B2'› outH_expand)
          hence "¬ ColH O2 A2' B2'" 
            by (metis ‹ColH O2 A2 A2'› ‹O2 ≠ A2'› ‹O2 ≠ B2'› assms(3) 
                colH_permut_312 colH_trans colH_trivial122)
          have "CongH A B A1' B1'" 
          proof -
            have "CongH PO A O1 A1'" 
              using ‹CongH O1 A1' PO A› ‹O1 ≠ A1'› ‹PO ≠ A› congH_perms by blast
            moreover have "CongH PO B O1 B1'" 
              by (simp add: ‹CongH O1 B1' PO B› ‹O1 ≠ B1'› congH_sym)
            moreover have "CongaH A PO B A1' O1 B1'" 
              using ‹PO ≠ A› ‹PO ≠ B› ‹outH O1 A1 A1'› ‹outH O1 B1 B1'› 
                assms(4) conga_out_conga outH_trivial by blast
            ultimately show ?thesis 
              using assms(1) th12 ‹ColH O1 A1' B1' ⟹ False› by blast
          qed
          have "CongH A B A2' B2'" 
          proof -
            have "CongH PO A O2 A2'" 
              using ‹CongH O2 A2' PO A› ‹O2 ≠ A2'› congH_sym by auto
            moreover have "CongH PO B O2 B2'" 
              by (simp add: ‹CongH O2 B2' PO B› ‹O2 ≠ B2'› congH_sym)
            moreover have "CongaH A PO B A2' O2 B2'" 
              using ‹PO ≠ A› ‹PO ≠ B› ‹outH O2 A2 A2'› ‹outH O2 B2 B2'› 
                assms(5) conga_out_conga outH_trivial by blast
            ultimately show ?thesis 
              using  assms(1) th12 ‹¬ ColH O2 A2' B2'› by blast
          qed
          have "CongH A1' B1' A2' B2'" 
            using ‹CongH A B A1' B1'› ‹CongH A B A2' B2'› cong_pseudo_transitivity by blast
          have "CongaH A1' O1 B1' A2' O2 B2'" 
          proof -
            have "CongH O1 A1' O2 A2'" 
              by (meson ‹CongH O1 A1' PO A› ‹CongH O2 A2' PO A› ‹O1 ≠ A1'› 
                  ‹O2 ≠ A2'› congH_sym cong_pseudo_transitivity)
            moreover have "CongH O1 B1' O2 B2'" 
              by (meson ‹CongH O1 B1' PO B› ‹CongH O2 B2' PO B› ‹O1 ≠ B1'› 
                  ‹O2 ≠ B2'› congH_sym cong_pseudo_transitivity)
            ultimately show ?thesis 
              using th18_aux ‹CongH A1' B1' A2' B2'› ‹ColH O1 A1' B1' ⟹ False› 
                ‹¬ ColH O2 A2' B2'› by blast
          qed
          hence "CongaH A1 O1 B1 A2 O2 B2" 
            using ‹O1 ≠ A1'› ‹O1 ≠ B1'› ‹O2 ≠ A2'› ‹O2 ≠ B2'› ‹outH O1 A1 A1'› 
              ‹outH O1 B1 B1'› ‹outH O2 A2 A2'› ‹outH O2 B2 B2'› conga_out_conga outH_sym by blast
        }
        hence "CongaH A1 O1 B1 A2 O2 B2" 
          using ‹O2 ≠ B2› ‹PO ≠ B› out_construction by blast
      }
      hence "CongaH A1 O1 B1 A2 O2 B2" 
        using ‹O1 ≠ B1› ‹PO ≠ B› out_construction by blast
    }
    hence "CongaH A1 O1 B1 A2 O2 B2" 
      using ‹O2 ≠ A2› ‹PO ≠ A› out_construction by blast
  }
  thus ?thesis 
    using ‹O1 ≠ A1› ‹PO ≠ A› out_construction by force
qed


lemma congaH_sym:
  assumes "¬ ColH A B C" and
    "¬ ColH D E F" and
    "CongaH A B C D E F"
  shows "CongaH D E F A B C" 
  by (meson assms(1) assms(2) assms(3) colH_permut_213 conga_refl th19)

lemma congaH_commr:
  assumes "¬ ColH A B C" and
    "¬ ColH D E F" and
    "CongaH A B C D E F"
  shows "CongaH A B C F E D" 
  using th19 [of _ _ _ B A C E F D]
  by (meson assms(1,2,3) colH_permut_132 colH_permut_213 conga_comm conga_permlr) 

lemma cong_preserves_col:
  assumes "BetH A B C" and
    "CongH A B A' B'" and
    "CongH B C B' C'" and
    "CongH A C A' C'" 
  shows "ColH A' B' C'" 
proof -
  have "ColH A B C" 
    by (simp add: assms(1) betH_colH)
  have "A ≠ B" 
    using assms(1) betH_distincts by blast
  have "C ≠ B" 
    using assms(1) betH_distincts by blast
  {
    assume "¬ ColH A' B' C'"
    {
      assume "A' = C'" 
      hence False 
        using ‹¬ ColH A' B' C'› colH_trivial121 by blast
    }
    then obtain B'' where "CongH A' B'' A B" and "outH A' C' B''" 
      using ‹A ≠ B› out_construction by blast
    hence "ColH A' C' B''" 
      using outH_expand by blast
    have "A' ≠ B''" 
      using ‹outH A' C' B''› out_distinct by blast
    have "outH A' B'' C'" 
      by (simp add: ‹A' ≠ B''› ‹outH A' C' B''› outH_sym)
    hence "BetH A' B'' C'" 
      using ‹A' ≠ B''› ‹CongH A' B'' A B› assms(1) assms(4) 
        betH_congH3_outH_betH congH_sym by blast
    have "A' ≠ B'" 
      using ‹¬ ColH A' B' C'› colH_trivial112 by auto
    obtain C'' where "BetH A' B' C''" and "CongH B' C'' B C" 
      using ‹A' ≠ B'› ‹C ≠ B› segment_constructionH by metis
    hence "ColH A' B' C''" 
      using betH_colH by force
    have "B' ≠ C''" 
      using ‹BetH A' B' C''› betH_distincts by blast
    have "A' ≠ C''" 
      using ‹BetH A' B' C''› not_betH121 by blast
    have "CongH B C B'' C'" 
      using ‹A' ≠ B''› ‹BetH A' B'' C'› ‹CongH A' B'' A B› assms(1) assms(4)
        congH_sym soustraction_betH by presburger
    have "CongH A' C'' A' C'" 
      by (meson ‹B' ≠ C''› ‹BetH A' B' C''› ‹ColH A B C› ‹ColH A' B' C''› 
          ‹CongH B' C'' B C› addition assms(1) assms(2) assms(4) bet_disjoint 
          congH_sym cong_pseudo_transitivity)
    have "¬ ColH A' C'' C'" 
      using ‹A' ≠ C''› ‹ColH A' B' C''› ‹¬ ColH A' B' C'› colH_permut_132 
        colH_trans colH_trivial121 by blast
    have "CongaH A' C'' C' A' C' C''" 
      by (simp add: ‹CongH A' C'' A' C'› ‹¬ ColH A' C'' C'› isosceles_congaH)         
    have "¬ ColH B' C'' C'" 
      by (meson ‹B' ≠ C''› ‹ColH A' B' C''› ‹¬ ColH A' B' C'› colH_permut_231
          colH_trans colH_trivial121)
    have "CongaH B' C'' C' B' C' C''" 
      by (meson ‹B' ≠ C''› ‹CongH B' C'' B C› ‹¬ ColH B' C'' C'› assms(3)
          congH_sym cong_pseudo_transitivity isosceles_congaH)
    have "CongaH A' C'' C' B' C'' C'" 
      using ‹A' ≠ C''› ‹BetH A' B' C''› ‹ColH A' B' C''› ‹¬ ColH A' B' C'› 
        ‹¬ ColH A' C'' C'› between_comm conga_out_conga conga_refl outH_def by blast
    have "CongaH A' C' C'' B' C' C''" 
    proof (rule th19 [of C'' A' C' C' A' C'' C' B' C''], insert ‹CongaH A' C'' C' A' C' C''›)
      show "¬ ColH C'' A' C'"
        using ‹¬ ColH A' C'' C'› colH_permut_213 by blast 
      show "¬ ColH C' A' C''" 
        using ‹¬ ColH C'' A' C'› colH_permut_321 by blast 
      show "¬ ColH C' B' C''"
        using ‹¬ ColH B' C'' C'› colH_permut_231 by blast
      show "CongaH A' C'' C' B' C' C''"
        by (metis (no_types) ‹CongaH A' C'' C' B' C'' C'› ‹CongaH B' C'' C' B' C' C''›
            ‹¬ ColH A' C'' C'› ‹¬ ColH B' C'' C'› ‹¬ ColH C' B' C''› ‹¬ ColH C'' A' C'› 
            colH_permut_321 congaH_sym th19) 
    qed
    have "outH C' A' B'"
    proof -
      have "¬ ColH B' C' C''" 
        using ‹¬ ColH B' C'' C'› colH_permut_132 by blast
      moreover have "¬ ColH A' C' C''" 
        using ‹¬ ColH A' C'' C'› colH_permut_132 by blast
      moreover have "CongaH A' C' C'' C'' C' A'" 
        by (simp add: calculation(2) conga_comm)
      moreover have "CongaH A' C' C'' C'' C' B'" 
        using ‹CongaH A' C' C'' B' C' C''› calculation(1) calculation(2) 
          congaH_commr by blast
      moreover have "same_side' B' A' C' C''" 
        by (metis ColH_def ‹BetH A' B' C''› between_comm calculation(1) 
            colH_trivial122 outH_def out_same_side')
      moreover have "same_side' B' B' C' C''" 
        using calculation(1) colH_permut_312 same_side_prime_refl by blast
      ultimately show ?thesis 
        using cong_4_uniqueness by blast
    qed
    hence False 
      using ‹¬ ColH A' B' C'› colH_permut_231 outH_col by blast
  }
  thus ?thesis by blast
qed

lemma cong_preserves_col_stronger:
  assumes "A ≠ B" and
    "A ≠ C" and
    "B ≠ C" and
    "ColH A B C" and
    "CongH A B A' B'" and
    "CongH B C B' C'" and
    "CongH A C A' C'"
  shows "ColH A' B' C'" 
  by (metis ncolH_expand assms(1) assms(2) assms(3) assms(4) assms(5) 
      assms(6) assms(7) between_one colH_permut_213 colH_permut_312 
      congH_permlr cong_preserves_col)

lemma betH_congH2__False:
  assumes "BetH A B C" and
    "BetH A' C' B'" and
    "CongH A B A' B'" and
    "CongH A C A' C'" 
  shows "False" 
proof -
  have "ColH A B C" 
    using assms(1) betH_colH by auto
  have "ColH A' C' B'" 
    by (simp add: assms(2) betH_colH)
  have "A ≠ B" 
    using assms(1) betH_distincts by blast
  have "C ≠ B" 
    using assms(1) betH_distincts by blast
  have "A' ≠ B'" 
    using assms(2) not_betH121 by force
  obtain C0 where "BetH A' B' C0" and "CongH B' C0 B C" 
    using ‹A' ≠ B'› ‹C ≠ B› segment_constructionH by metis
  hence "CongH A' C0 A C" 
    using ‹A ≠ B› addition_betH assms(1) assms(3) congH_sym by blast
  have "BetH A' C' C0" 
    using ‹BetH A' B' C0› assms(2) betH_trans0 by blast
  moreover have "CongH A' C' A' C0" 
    by (metis ‹BetH A' B' C0› ‹CongH A' C0 A C› assms(4) betH_distincts
        congH_sym cong_pseudo_transitivity)
  ultimately show ?thesis 
    by (simp add: betH_not_congH)
qed

lemma cong_preserves_bet: 
  assumes "A' ≠ B'" and
    "B' ≠ C'" and
    "A'≠C'" and
    "BetH A B C" and
    "CongH A B A' B'" and
    "CongH B C B' C'" and
    "CongH A C A' C'"
  shows "BetH A' B' C'" 
  by (meson assms(1) assms(2) assms(3) assms(4) assms(5) assms(6) 
      assms(7) bet_cong3_bet cong_preserves_col)

lemma axiom_five_segmentsH:
  assumes "A ≠ D" and
    "A' ≠ D'" and
    "B ≠ D" and
    "B' ≠ D'" and
    "C ≠ D" and
    "C' ≠ D'" and
    "CongH A B A' B'" and
    "CongH B C B' C'" and
    "CongH A D A' D'" and
    "CongH B D B' D'" and
    "BetH A B C" and
    "BetH A' B' C'" and
    "A' ≠ D'"
  shows "CongH C D C' D'" 
proof -
  have "ColH A B C" 
    by (simp add: assms(11) betH_colH)
  have "ColH A' B' C'" 
    by (simp add: assms(12) betH_colH)
  have "A ≠ B" 
    using assms(11) betH_distincts by blast
  have "A ≠ C" 
    using assms(11) not_betH121 by blast
  have "A' ≠ B'" 
    using assms(12) betH_distincts by auto
  have "A' ≠ C'" 
    using assms(12) not_betH121 by blast
  have "C' ≠ B'" 
    using assms(12) betH_distincts by blast
  have "CongH A C A' C'" 
    using addition_betH assms(11) assms(12) assms(7) assms(8) by blast
  {
    assume "ColH A B D"
    hence "BetH A B D ∨ BetH B D A ∨ BetH B A D" 
      by (simp add: ‹A ≠ B› assms(1) assms(3) between_one)
    moreover
    {
      assume "BetH A B D"
      hence "BetH A' B' D'" 
        using ‹A' ≠ B'› assms(10) assms(2) assms(4) assms(7) assms(9) 
          cong_preserves_bet by blast
      hence "BetH A' D' C' ∨ BetH A' C' D'" 
        using  assms(12) assms(6) out2_out1 by auto
      moreover
      {
        assume "BetH A' D' C'" 
        hence "BetH A D C" 
          by (meson ‹BetH A B D› ‹CongH A C A' C'› assms(11) assms(5)
              assms(9) betH_congH2__False out2_out1)
        hence ?thesis 
          using ‹BetH A' D' C'› ‹CongH A C A' C'› assms(9) betH_colH 
            congH_permlr soustraction_betH by presburger
      }
      moreover
      {
        assume "BetH A' C' D'" 
        hence "BetH A C D" 
          by (meson ‹BetH A B D› ‹CongH A C A' C'› assms(11) assms(5)
              assms(9) betH_congH2__False out2_out1)
        hence ?thesis 
          using ‹BetH A' C' D'› ‹CongH A C A' C'› assms(9) 
            soustraction_betH by blast
      }
      ultimately have ?thesis 
        by blast
    }
    moreover
    {
      assume "BetH B D A"
      hence "BetH B' D' A'" 
        by (metis ‹A' ≠ B'› assms(10) assms(2) assms(4) assms(7)
            assms(9) congH_permlr cong_preserves_bet)
      hence "BetH C D A" 
        using betH_trans0 ‹BetH B D A› assms(11) between_comm by blast
      hence "BetH C' D' A'" 
        using betH_trans0 ‹BetH B' D' A'› assms(12) between_comm by blast
      have "BetH A D C" 
        by (simp add: ‹BetH C D A› between_comm)
      moreover have "BetH A' D' C'" 
        by (simp add: ‹BetH C' D' A'› between_comm)
      ultimately have ?thesis 
        using ‹CongH A C A' C'› assms(9) betH_expand congH_permlr 
          soustraction_betH by presburger
    }
    moreover
    {
      assume "BetH B A D"
      hence "BetH B' A' D'" 
        by (metis ‹A' ≠ B'› assms(10) assms(2) assms(4) assms(7) assms(9) 
            congH_permlr cong_preserves_bet)
      have "BetH C' B' D'" 
        using ‹BetH B' A' D'› assms(12) betH_trans between_comm by blast
      have "BetH C B D"         
        using ‹BetH B A D› assms(11) betH_trans between_comm by blast
      moreover have "CongH C B C' B'"         
        using ‹C' ≠ B'› assms(8) congH_permlr by presburger
      ultimately have ?thesis 
        using ‹BetH C' B' D'› assms(10) addition_betH by blast
    }
    ultimately have ?thesis 
      by blast
  }
  moreover
  {
    assume "¬ ColH A B D" 
    hence "¬ ColH A' B' D'" 
      using cong_preserves_col_stronger ‹A ≠ B› ‹A' ≠ B'› assms(1) assms(10)
        assms(2) assms(3) assms(4) assms(7) assms(9) congH_sym by blast
    hence "CongaH B A D B' A' D'" 
      using ‹¬ ColH A B D› assms(10) assms(7) assms(9) th18_aux by blast
    have "¬ ColH A C D" 
      using ‹A ≠ C› ‹ColH A B C› ‹¬ ColH A B D› colH_permut_132 colH_trans 
        colH_trivial121 by blast
    moreover have "¬ ColH A' C' D'" 
      using ‹A' ≠ C'› ‹ColH A' B' C'› ‹¬ ColH A' B' D'› colH_permut_132 
        colH_trans colH_trivial121 by blast
    moreover have "CongaH C A D C' A' D'" 
      using ‹CongaH B A D B' A' D'› assms(1) assms(11) assms(12) assms(2)
        conga_out_conga outH_def by blast
    ultimately have ?thesis 
      using ‹CongH A C A' C'› assms(9) th12 by blast
  }
  ultimately show ?thesis 
    by blast
qed

lemma five_segment:
  assumes "Cong A B A' B'" and
    "Cong B C B' C'" and
    "Cong A D A' D'" and
    "Cong B D B' D'" and
    "Bet A B C" and
    "Bet A' B' C'" and
    "A ≠ B"
  shows "Cong C D C' D'" 
proof -
  {
    assume "BetH A B C"
    {
      assume "BetH A' B' C'"
      have "ColH A B C" 
        using ‹BetH A B C› betH_colH by blast
      have "ColH A' B' C'" 
        by (simp add: assms(6) bet_colH)
      have "C ≠ B" 
        using ‹BetH A B C› betH_distincts by blast
      have "A ≠ C" 
        using ‹BetH A B C› betH_distincts by blast
      have "A' ≠ B'" 
        using ‹BetH A' B' C'› betH_distincts by blast
      have "C' ≠ B'" 
        using ‹BetH A' B' C'› betH_distincts by blast
      have "A' ≠ C'" 
        using ‹BetH A' B' C'› betH_distincts by blast
      have "CongH A B A' B'" 
        using Cong_def ‹A' ≠ B'› assms(1) by presburger
      have "CongH B C B' C'" 
        using Cong_def ‹C ≠ B› assms(2) by blast
      have "CongH A D A' D' ∧ A ≠ D ∧ A' ≠ D' ∨ (A = D ∧ A' = D')" 
        using Cong_def assms(3) by force
      moreover
      have "CongH B D B' D' ∧ B ≠ D ∧ B'≠ D' ∨ (B = D ∧ B' = D')" 
        using Cong_def assms(4) by presburger
      {
        assume "CongH A D A' D' ∧ A ≠ D ∧ A' ≠ D'"
        hence "CongH A D A' D'" 
          by blast
        have "A ≠ D" 
          by (simp add: ‹CongH A D A' D' ∧ A ≠ D ∧ A' ≠ D'›)
        have "A' ≠ D'" 
          by (simp add: ‹CongH A D A' D' ∧ A ≠ D ∧ A' ≠ D'›)
        {
          assume "CongH B D B' D' ∧ B ≠ D ∧ B'≠ D'"
          hence "CongH B D B' D'" 
            by blast
          have "B ≠ D" 
            by (simp add: ‹CongH B D B' D' ∧ B ≠ D ∧ B' ≠ D'›)
          have "B'≠ D'"
            by (simp add: ‹CongH B D B' D' ∧ B ≠ D ∧ B' ≠ D'›)
          {
            assume "C = D"
            have "CongH B' C' B' D'" 
              using ‹C = D› ‹CongH B C B' C'› ‹CongH B D B' D' ∧ B ≠ D ∧ B' ≠ D'› 
                cong_pseudo_transitivity by blast
            hence "C' = D'" 
              using ‹A' ≠ B'› ‹A' ≠ D'› ‹B' ≠ D'› ‹BetH A B C› ‹BetH A' B' C'› 
                ‹C = D› ‹CongH A B A' B'› ‹CongH A D A' D'› ‹CongH B D B' D'› 
                cong_preserves_bet construction_uniqueness by blast
            hence ?thesis 
              by (simp add: Cong_def ‹C = D›)
          }
          moreover
          {
            assume "C ≠ D"
            {
              assume "C' = D'"
              hence "CongH B D B C" 
                by (metis ‹B ≠ D› ‹C ≠ B› ‹CongH B C B' C'› ‹CongH B D B' D'›
                    congH_sym cong_pseudo_transitivity)
              have "BetH A B D" 
                using ‹A ≠ D› ‹B ≠ D› ‹BetH A' B' C'› ‹C' = D'› ‹CongH A B A' B'› 
                  ‹CongH A D A' D'› ‹CongH B D B' D'› assms(7) congH_sym cong_preserves_bet by presburger
              moreover have "CongH B C B D" 
                using ‹B ≠ D› ‹CongH B D B C› congH_sym by auto
              ultimately have "C = D" 
                using construction_uniqueness ‹BetH A B C› by presburger
              hence False 
                using ‹C ≠ D› by blast
            }
            hence "C' ≠ D'" 
              by blast          
            hence ?thesis 
              by (meson Cong_def ‹BetH A B C› ‹BetH A' B' C'› ‹CongH A B A' B'›
                  ‹CongH A D A' D' ∧ A ≠ D ∧ A' ≠ D'› ‹CongH B C B' C'› 
                  ‹CongH B D B' D' ∧ B ≠ D ∧ B' ≠ D'› axiom_five_segmentsH calculation)
          }
          ultimately have ?thesis 
            by blast
        }
        moreover
        {
          assume "B = D ∧ B' = D'" 
          hence ?thesis 
            using Cong_def ‹C ≠ B› ‹C' ≠ B'› ‹CongH B C B' C'› congH_permlr by presburger
        }
        ultimately have ?thesis 
          using ‹CongH B D B' D' ∧ B ≠ D ∧ B' ≠ D' ∨ B = D ∧ B' = D'› by fastforce
      }
      moreover
      {
        assume "A = D ∧ A' = D'"
        hence ?thesis 
          using Cong_def ‹A ≠ C› ‹A' ≠ C'› ‹BetH A B C› ‹BetH A' B' C'› 
            ‹CongH A B A' B'› ‹CongH B C B' C'› addition_betH congH_permlr by presburger
      }
      ultimately have ?thesis 
        by blast
    }
    moreover 
    {
      assume "A' = B'"
      hence ?thesis 
        using assms(1) assms(7) cong_identity by blast
    }
    moreover
    {
      assume "B' = C'"
      hence ?thesis 
        using Cong_def ‹BetH A B C› assms(2) betH_to_bet by auto
    }
    ultimately have ?thesis 
      using Bet_def assms(6) by blast
  }
  moreover 
  {
    assume "A = B"
    hence ?thesis 
      using assms(7) by blast
  }
  moreover
  {
    assume "B = C"
    hence ?thesis 
      using Cong_def assms(2) assms(4) by presburger
  }
  ultimately show ?thesis 
    using Bet_def assms(5) by blast
qed

lemma bet_comm:
  assumes "Bet A B C"
  shows "Bet C B A" 
  using Bet_def assms between_comm by presburger

lemma bet_trans:
  assumes "Bet A B D" and
    "Bet B C D"
  shows "Bet A B C" 
proof -
  {
    assume "BetH A B D"
    hence ?thesis 
      using Bet_def assms(2) betH_trans0 between_comm by blast
  }
  moreover
  {
    assume "A = B ∨ B = D"
    hence ?thesis 
      using Bet_def assms(2) bet_identity by blast
  }
  ultimately show ?thesis 
    using Bet_def assms(1) by blast
qed

lemma cong_transitivity:
  assumes "Cong A B E F" and 
    "Cong C D E F"
  shows "Cong A B C D" 
  using assms(1) assms(2) cong_sym cong_trans by blast

lemma cong_permT:
  shows "Cong A B B A" 
  by (metis Cong_def congH_perm)

lemma pasch_general_case:
  assumes "Bet A P C" and
    "Bet B Q C" and
    "A ≠ P" and
    "P ≠ C" and
    "B ≠ Q" and
    "Q ≠ C" and
    "¬ (Bet A B C ∨ Bet B C A ∨ Bet C A B)"
  shows "∃ x. Bet P x B ∧ Bet Q x A"
proof (cases "A = B")
  case True
  thus ?thesis
    using Bet_def by auto
next
  case False
  {
    assume "B = C"
    hence ?thesis 
      using Bet_def assms(7) by presburger
  }
  moreover
  {
    assume "B ≠ C"
    {
      assume "A = C" 
      hence ?thesis 
        using Bet_def assms(7) by blast
    }
    moreover
    {
      assume "A ≠ C"
      have "ColH A P C" 
        by (simp add: assms(1) bet_colH)
      {
        assume "ColH B C P"
        hence "ColH A B C" 
          by (metis colH_permut_231 colH_trivial121 ‹ColH A P C› assms(4) inter_uniquenessH)
        hence False 
          by (metis Bet_def assms(7) between_comm between_one)
      }
      hence "¬ ColH B C P" 
        by blast
      hence ?thesis 
        using assms(1) assms(2) inner_pasch_aux by blast
    }
    ultimately have ?thesis 
      by blast
  }
  ultimately show ?thesis 
    by blast
qed

lemma lower_dim_l:
  shows "¬ (Bet PP PQ PR ∨ Bet PQ PR PP ∨ Bet PR PP PQ)" 
  using bet_colH colH_permut_231 lower_dim_2 by blast

lemma ColH_bets:
  assumes "ColH A B C"
  shows "Bet A B C ∨ Bet B C A ∨ Bet C A B" 
  by (metis Bet_def assms bet_comm between_one)

end
end