Require Import GeoCoq.Axioms.parallel_postulates.
Require Import GeoCoq.Meta_theory.Parallel_postulates.tarski_s_euclid_remove_degenerated_cases.
Require Import GeoCoq.Tarski_dev.Ch12_parallel.

Section SPP_tarski.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma impossible_case_5 : forall P Q R S T U I,
  BetS P T Q ->
  BetS R T S ->
  BetS Q U R ->
  ~ Col P Q S ->
  ~ Col P R U ->
  Par P R Q S ->
  Par P S Q R ->
  Bet S Q I ->
  Bet U I P ->
  False.
Proof.
(* Goal: forall (P Q R S T U I : @Tpoint Tn) (_ : @BetS Tn P T Q) (_ : @BetS Tn R T S) (_ : @BetS Tn Q U R) (_ : not (@Col Tn P Q S)) (_ : not (@Col Tn P R U)) (_ : @Par Tn P R Q S) (_ : @Par Tn P S Q R) (_ : @Bet Tn S Q I) (_ : @Bet Tn U I P), False *)
intros P Q R S T U I HPTQ HRTS HQUR HNC HNC' HPar1 HPar2 HSQI HPUI.
(* Goal: False *)
apply BetSEq in HPTQ; apply BetSEq in HRTS; apply BetSEq in HQUR.
assert (HTS : TS Q S P U) by (assert_diffs; spliter; assert_cols; repeat split;
                                     Col; try (exists I; Col; Between); intro; apply HNC'; ColR).
(* Goal: False *)
apply l9_9 in HTS; apply HTS.
(* Goal: @OS Tn Q S P U *)
apply one_side_transitivity with R.

(* Goal: @OS Tn D A X B *)
  {
(* Goal: @OS Tn Q S P R *)
  apply l12_6; apply par_not_col_strict with P; Col; Par.
  }

(* Goal: @OS Tn D A X B *)
  {
(* Goal: @OS Tn Q S R U *)
  assert (HQS : Q <> S) by (assert_diffs; assumption).
(* Goal: @OS Tn Q S R U *)
  assert (HQSQ : Col Q S Q) by Col.
(* Goal: @OS Tn Q S R U *)
  assert (HRUQ : Col R U Q) by (spliter; assert_cols; Col).
(* Goal: @OS Tn Q S R U *)
  rewrite (l9_19 Q S R U Q HQSQ HRUQ).
(* Goal: and (@Out Tn Q R U) (not (@Col Tn Q S R)) *)
  split; spliter; try (intro; apply HNC; assert_cols; ColR); repeat split; Between.
  }
Qed.

Lemma impossible_case_6 : forall P Q R S T U I,
  BetS P T Q ->
  BetS R T S ->
  BetS Q U R ->
  ~ Col P Q S ->
  ~ Col P R U ->
  Par P R Q S ->
  Par P S Q R ->
  Bet S Q I ->
  Bet I P U ->
  False.
Proof.
(* Goal: forall (P Q R S T U I : @Tpoint Tn) (_ : @BetS Tn P T Q) (_ : @BetS Tn R T S) (_ : @BetS Tn Q U R) (_ : not (@Col Tn P Q S)) (_ : not (@Col Tn P R U)) (_ : @Par Tn P R Q S) (_ : @Par Tn P S Q R) (_ : @Bet Tn S Q I) (_ : @Bet Tn U I P), False *)
intros P Q R S T U I HPTQ HRTS HQUR HNC HNC' HPar1 HPar2 HSQI HPUI.
(* Goal: False *)
apply BetSEq in HPTQ; apply BetSEq in HRTS; apply BetSEq in HQUR.
apply between_symmetry in HPUI.
destruct (inner_pasch S U I Q P HSQI HPUI) as [J [HBet1 HBet2]].
assert (HParS : Par_strict P S Q U).
(* Goal: @OS Tn D A X B *)
  {
  apply par_not_col_strict with R.

(* Goal: @OS Tn D A X B *)
    {
    spliter; assert_cols.
    apply par_col_par with R; Par.
    ColR.
    }

(* Goal: @OS Tn D A X B *)
    {
    spliter; assert_cols; ColR.
    }

(* Goal: @OS Tn D A X B *)
    {
    intro; apply HNC.
    spliter; assert_cols; ColR.
    }
  }
apply HParS; exists J; assert_cols; Col.
Qed.

Lemma impossible_case_7 : forall P Q R S T U I,
  BetS P T Q ->
  BetS R T S ->
  BetS Q U R ->
  ~ Col P Q S ->
  ~ Col P R U ->
  Par P R Q S ->
  Par P S Q R ->
  Col P U I ->
  Bet Q I S ->
  False.
Proof.
(* Goal: forall (P Q R S T U I : @Tpoint Tn) (_ : @BetS Tn P T Q) (_ : @BetS Tn R T S) (_ : @BetS Tn Q U R) (_ : not (@Col Tn P Q S)) (_ : not (@Col Tn P R U)) (_ : @Par Tn P R Q S) (_ : @Par Tn P S Q R) (_ : @Col Tn P U I) (_ : @Bet Tn I S Q), False *)
intros P Q R S T U I HPTQ HRTS HQUR HNC HNC' HPar1 HPar2 HPUI HSQI.
(* Goal: False *)
apply BetSEq in HPTQ; apply BetSEq in HRTS; apply BetSEq in HQUR.
(* Goal: False *)
elim (eq_dec_points I S); intro HIS; treat_equalities.

(* Goal: @OS Tn D A X B *)
  {
  assert (HParS : Par_strict Q R P I) by (apply par_not_col_strict with P; Col; Par; unfold BetS in *;
                                          spliter; assert_cols; intro; apply HNC'; ColR).
(* Goal: False *)
  apply HParS; exists U; spliter; assert_cols; Col.
  }

(* Goal: @OS Tn D A X B *)
  {
  assert (HTS : TS P U Q S) by (assert_diffs; spliter; assert_cols; repeat split;
                                       Col; try (exists I; Col; Between); intro; apply HNC; ColR).
(* Goal: False *)
  apply l9_9 in HTS; apply HTS.
(* Goal: @OS Tn P U Q S *)
  exists R; split.

(* Goal: @OS Tn D A X B *)
    {
(* Goal: @TS Tn P U S R *)
    spliter; assert_diffs; assert_cols.
(* Goal: and (not (@Col Tn R P U)) (@ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T P U) (@Bet Tn S T R))) *)
    split; try (intro; apply HNC; ColR).
(* Goal: and (not (@Col Tn R P U)) (@ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T P U) (@Bet Tn S T R))) *)
    split; try (intro; apply HNC; ColR).
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T P U) (@Bet Tn Q T R)) *)
    exists U; Col; Between.
    }

(* Goal: @OS Tn D A X B *)
    {
(* Goal: @TS Tn P U S R *)
    destruct HPTQ as [HPTQ HDiff1].
(* Goal: @TS Tn P U S R *)
    destruct HQUR as [HQUR HDiff2].
(* Goal: @TS Tn P U S R *)
    apply between_symmetry in HQUR.
(* Goal: @TS Tn P U S R *)
    destruct (inner_pasch R P Q U T HQUR HPTQ) as [J [HPJU HRJT]].
(* Goal: @TS Tn P U S R *)
    assert (HRJS : Bet R J S) by (spliter; eBetween).
(* Goal: @TS Tn P U S R *)
    spliter; assert_diffs; assert_cols.
(* Goal: and (not (@Col Tn R P U)) (@ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T P U) (@Bet Tn S T R))) *)
    split; try (intro; apply HNC; ColR).
(* Goal: and (not (@Col Tn R P U)) (@ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T P U) (@Bet Tn S T R))) *)
    split; try (intro; apply HNC; ColR).
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T P U) (@Bet Tn S T R)) *)
    exists J; split; Col; Between.
    }
  }
Qed.

Lemma impossible_case_8 : forall P Q R S T U I,
  BetS P T Q ->
  BetS R T S ->
  BetS Q U R ->
  ~ Col P Q S ->
  ~ Col P R U ->
  Par P R Q S ->
  Par P S Q R ->
  Col P U I ->
  Bet I S Q ->
  False.
Proof.
(* Goal: forall (P Q R S T U I : @Tpoint Tn) (_ : @BetS Tn P T Q) (_ : @BetS Tn R T S) (_ : @BetS Tn Q U R) (_ : not (@Col Tn P Q S)) (_ : not (@Col Tn P R U)) (_ : @Par Tn P R Q S) (_ : @Par Tn P S Q R) (_ : @Col Tn P U I) (_ : @Bet Tn I S Q), False *)
intros P Q R S T U I HPTQ HRTS HQUR HNC HNC' HPar1 HPar2 HPUI HSQI.
(* Goal: False *)
apply BetSEq in HPTQ; apply BetSEq in HRTS; apply BetSEq in HQUR.
(* Goal: False *)
elim HPUI; clear HPUI; intro HPUI.

(* Goal: @OS Tn D A X B *)
  {
  assert (H : Par_strict P S Q R) by (apply par_not_col_strict with Q; Col; Par; unfold BetS in *;
                                      spliter; assert_cols; intro; apply HNC'; ColR); apply H.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X P S) (@Col Tn X Q R)) *)
  apply between_symmetry in HSQI.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X P S) (@Col Tn X Q R)) *)
  destruct (inner_pasch P Q I U S HPUI HSQI) as [J [HQJU HPJS]]; exists J.
  spliter; assert_diffs; assert_cols; split; Col; ColR.
  }

(* Goal: @OS Tn D A X B *)
  {
(* Goal: False *)
  elim HPUI; clear HPUI; intro HPUI.

(* Goal: @OS Tn D A X B *)
    {
    assert (H : Par_strict P S Q R) by (apply par_not_col_strict with Q; Col; Par; unfold BetS in *;
                                        spliter; assert_cols; intro; apply HNC'; ColR); apply H.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X P S) (@Col Tn X Q R)) *)
    apply between_symmetry in HSQI.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X P S) (@Col Tn X Q R)) *)
    destruct (outer_pasch U Q I P S HPUI HSQI) as [J [HQJU HPSJ]]; exists J.
    spliter; assert_diffs; assert_cols; split; Col; ColR.
    }

(* Goal: @OS Tn D A X B *)
    {
    assert (H : Par_strict P R Q S) by (apply par_not_col_strict with Q; Col; Par; unfold BetS in *;
                                        spliter; assert_cols; intro; apply HNC'; ColR); apply H.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X P R) (@Col Tn X Q S)) *)
    destruct HQUR as [HQUR HDiff].
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X P R) (@Col Tn X Q S)) *)
    destruct (outer_pasch Q I U R P HQUR HPUI) as [J [HQJI HRPJ]]; exists J.
(* Goal: and (@Col Tn J P R) (@Col Tn J Q S) *)
    spliter; assert_diffs; assert_cols; split; Col.
    elim (eq_dec_points Q I); intro HQI; treat_equalities; Col; ColR.
    }
  }
Qed.

Lemma strong_parallel_postulate_implies_tarski_s_euclid_aux :
  strong_parallel_postulate ->
  (forall A B C D T,
   A <> B ->
   A <> C ->
   A <> D ->
   A <> T ->
   B <> C ->
   B <> D ->
   B <> T ->
   C <> D ->
   C <> T ->
   D <> T ->
   ~ Col A B C ->
   Bet A D T ->
   Bet B D C ->
   exists B', exists B'', exists MB, exists X, Bet A B X /\ Par_strict B C T X /\
   BetS B MB T /\ BetS B' MB B'' /\
   Cong B MB T MB /\ Cong B' MB B'' MB /\
   Col B B' D /\ Bet B'' T X /\
   B <> B' /\ B'' <> T).
Proof.
(* Goal: forall (_ : @strong_parallel_postulate Tn) (A B C D T : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) A C)) (_ : not (@eq (@Tpoint Tn) A D)) (_ : not (@eq (@Tpoint Tn) A T)) (_ : not (@eq (@Tpoint Tn) B C)) (_ : not (@eq (@Tpoint Tn) B D)) (_ : not (@eq (@Tpoint Tn) B T)) (_ : not (@eq (@Tpoint Tn) C D)) (_ : not (@eq (@Tpoint Tn) C T)) (_ : not (@eq (@Tpoint Tn) D T)) (_ : not (@Col Tn A B C)) (_ : @Bet Tn A D T) (_ : @Bet Tn B D C), @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => @ex (@Tpoint Tn) (fun B'' : @Tpoint Tn => @ex (@Tpoint Tn) (fun MB : @Tpoint Tn => @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A B X) (and (@Par_strict Tn B C T X) (and (@BetS Tn B MB T) (and (@BetS Tn B' MB B'') (and (@Cong Tn B MB T MB) (and (@Cong Tn B' MB B'' MB) (and (@Col Tn B B' D) (and (@Bet Tn B'' T X) (and (not (@eq (@Tpoint Tn) B B')) (not (@eq (@Tpoint Tn) B'' T)))))))))))))) *)
intros HSPP A B C D T HAB HAC HAD HAT HBC HBD HBT HCD HCT HDT HABC HADT HBDC.
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => @ex (@Tpoint Tn) (fun B'' : @Tpoint Tn => @ex (@Tpoint Tn) (fun MB : @Tpoint Tn => @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A B X) (and (@Par_strict Tn B C T X) (and (@BetS Tn B MB T) (and (@BetS Tn B' MB B'') (and (@Cong Tn B MB T MB) (and (@Cong Tn B' MB B'' MB) (and (@Col Tn B B' D) (and (@Bet Tn B'' T X) (and (not (@eq (@Tpoint Tn) B B')) (not (@eq (@Tpoint Tn) B'' T)))))))))))))) *)
destruct (symmetric_point_construction D B) as [B' HB'].
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => @ex (@Tpoint Tn) (fun B'' : @Tpoint Tn => @ex (@Tpoint Tn) (fun MB : @Tpoint Tn => @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A B X) (and (@Par_strict Tn B C T X) (and (@BetS Tn B MB T) (and (@BetS Tn B' MB B'') (and (@Cong Tn B MB T MB) (and (@Cong Tn B' MB B'' MB) (and (@Col Tn B B' D) (and (@Bet Tn B'' T X) (and (not (@eq (@Tpoint Tn) B B')) (not (@eq (@Tpoint Tn) B'' T)))))))))))))) *)
destruct (midpoint_distinct_2 B D B' HBD HB') as [HB'D HBB'].
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => @ex (@Tpoint Tn) (fun B'' : @Tpoint Tn => @ex (@Tpoint Tn) (fun MB : @Tpoint Tn => @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A B X) (and (@Par_strict Tn B C T X) (and (@BetS Tn B MB T) (and (@BetS Tn B' MB B'') (and (@Cong Tn B MB T MB) (and (@Cong Tn B' MB B'' MB) (and (@Col Tn B B' D) (and (@Bet Tn B'' T X) (and (not (@eq (@Tpoint Tn) B B')) (not (@eq (@Tpoint Tn) B'' T)))))))))))))) *)
destruct HB' as [HBDB' HCong1].
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => @ex (@Tpoint Tn) (fun B'' : @Tpoint Tn => @ex (@Tpoint Tn) (fun MB : @Tpoint Tn => @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A B X) (and (@Par_strict Tn B C T X) (and (@BetS Tn B MB T) (and (@BetS Tn B' MB B'') (and (@Cong Tn B MB T MB) (and (@Cong Tn B' MB B'' MB) (and (@Col Tn B B' D) (and (@Bet Tn B'' T X) (and (not (@eq (@Tpoint Tn) B B')) (not (@eq (@Tpoint Tn) B'' T)))))))))))))) *)
apply between_symmetry in HADT.
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => @ex (@Tpoint Tn) (fun B'' : @Tpoint Tn => @ex (@Tpoint Tn) (fun MB : @Tpoint Tn => @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A B X) (and (@Par_strict Tn B C T X) (and (@BetS Tn B MB T) (and (@BetS Tn B' MB B'') (and (@Cong Tn B MB T MB) (and (@Cong Tn B' MB B'' MB) (and (@Col Tn B B' D) (and (@Bet Tn B'' T X) (and (not (@eq (@Tpoint Tn) B B')) (not (@eq (@Tpoint Tn) B'' T)))))))))))))) *)
apply between_symmetry in HBDB'.
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => @ex (@Tpoint Tn) (fun B'' : @Tpoint Tn => @ex (@Tpoint Tn) (fun MB : @Tpoint Tn => @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A B X) (and (@Par_strict Tn B C T X) (and (@BetS Tn B MB T) (and (@BetS Tn B' MB B'') (and (@Cong Tn B MB T MB) (and (@Cong Tn B' MB B'' MB) (and (@Col Tn B B' D) (and (@Bet Tn B'' T X) (and (not (@eq (@Tpoint Tn) B B')) (not (@eq (@Tpoint Tn) B'' T)))))))))))))) *)
destruct (outer_pasch T B' D A B HADT HBDB') as [B''' [HTB'''B' HABB''']].
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => @ex (@Tpoint Tn) (fun B'' : @Tpoint Tn => @ex (@Tpoint Tn) (fun MB : @Tpoint Tn => @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A B X) (and (@Par_strict Tn B C T X) (and (@BetS Tn B MB T) (and (@BetS Tn B' MB B'') (and (@Cong Tn B MB T MB) (and (@Cong Tn B' MB B'' MB) (and (@Col Tn B B' D) (and (@Bet Tn B'' T X) (and (not (@eq (@Tpoint Tn) B B')) (not (@eq (@Tpoint Tn) B'' T)))))))))))))) *)
destruct (midpoint_existence B T) as [MB HMB].
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => @ex (@Tpoint Tn) (fun B'' : @Tpoint Tn => @ex (@Tpoint Tn) (fun MB : @Tpoint Tn => @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A B X) (and (@Par_strict Tn B C T X) (and (@BetS Tn B MB T) (and (@BetS Tn B' MB B'') (and (@Cong Tn B MB T MB) (and (@Cong Tn B' MB B'' MB) (and (@Col Tn B B' D) (and (@Bet Tn B'' T X) (and (not (@eq (@Tpoint Tn) B B')) (not (@eq (@Tpoint Tn) B'' T)))))))))))))) *)
destruct (midpoint_distinct_1 MB B T HBT HMB) as [HBMB HMBT].
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => @ex (@Tpoint Tn) (fun B'' : @Tpoint Tn => @ex (@Tpoint Tn) (fun MB : @Tpoint Tn => @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A B X) (and (@Par_strict Tn B C T X) (and (@BetS Tn B MB T) (and (@BetS Tn B' MB B'') (and (@Cong Tn B MB T MB) (and (@Cong Tn B' MB B'' MB) (and (@Col Tn B B' D) (and (@Bet Tn B'' T X) (and (not (@eq (@Tpoint Tn) B B')) (not (@eq (@Tpoint Tn) B'' T)))))))))))))) *)
destruct HMB as [HBMBT HCong2].
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => @ex (@Tpoint Tn) (fun B'' : @Tpoint Tn => @ex (@Tpoint Tn) (fun MB : @Tpoint Tn => @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A B X) (and (@Par_strict Tn B C T X) (and (@BetS Tn B MB T) (and (@BetS Tn B' MB B'') (and (@Cong Tn B MB T MB) (and (@Cong Tn B' MB B'' MB) (and (@Col Tn B B' D) (and (@Bet Tn B'' T X) (and (not (@eq (@Tpoint Tn) B B')) (not (@eq (@Tpoint Tn) B'' T)))))))))))))) *)
destruct (symmetric_point_construction B' MB) as [B'' HB''].
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => @ex (@Tpoint Tn) (fun B'' : @Tpoint Tn => @ex (@Tpoint Tn) (fun MB : @Tpoint Tn => @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A B X) (and (@Par_strict Tn B C T X) (and (@BetS Tn B MB T) (and (@BetS Tn B' MB B'') (and (@Cong Tn B MB T MB) (and (@Cong Tn B' MB B'' MB) (and (@Col Tn B B' D) (and (@Bet Tn B'' T X) (and (not (@eq (@Tpoint Tn) B B')) (not (@eq (@Tpoint Tn) B'' T)))))))))))))) *)
assert (HB'MB : MB <> B').
(* Goal: @OS Tn D A X B *)
  {
(* Goal: not (@eq (@Tpoint Tn) MB B') *)
  assert (H : ~ Col B' D MB) by (intro; apply HABC; assert_cols; ColR).
(* Goal: not (@eq (@Tpoint Tn) B''' T) *)
  intro; treat_equalities; apply H; Col.
  }
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => @ex (@Tpoint Tn) (fun B'' : @Tpoint Tn => @ex (@Tpoint Tn) (fun MB : @Tpoint Tn => @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A B X) (and (@Par_strict Tn B C T X) (and (@BetS Tn B MB T) (and (@BetS Tn B' MB B'') (and (@Cong Tn B MB T MB) (and (@Cong Tn B' MB B'' MB) (and (@Col Tn B B' D) (and (@Bet Tn B'' T X) (and (not (@eq (@Tpoint Tn) B B')) (not (@eq (@Tpoint Tn) B'' T)))))))))))))) *)
destruct (midpoint_distinct_2 MB B' B'' HB'MB HB'') as [HB'B'' HB''MB].
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => @ex (@Tpoint Tn) (fun B'' : @Tpoint Tn => @ex (@Tpoint Tn) (fun MB : @Tpoint Tn => @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A B X) (and (@Par_strict Tn B C T X) (and (@BetS Tn B MB T) (and (@BetS Tn B' MB B'') (and (@Cong Tn B MB T MB) (and (@Cong Tn B' MB B'' MB) (and (@Col Tn B B' D) (and (@Bet Tn B'' T X) (and (not (@eq (@Tpoint Tn) B B')) (not (@eq (@Tpoint Tn) B'' T)))))))))))))) *)
destruct HB'' as [HB'MBB'' HCong3].
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => @ex (@Tpoint Tn) (fun B'' : @Tpoint Tn => @ex (@Tpoint Tn) (fun MB : @Tpoint Tn => @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A B X) (and (@Par_strict Tn B C T X) (and (@BetS Tn B MB T) (and (@BetS Tn B' MB B'') (and (@Cong Tn B MB T MB) (and (@Cong Tn B' MB B'' MB) (and (@Col Tn B B' D) (and (@Bet Tn B'' T X) (and (not (@eq (@Tpoint Tn) B B')) (not (@eq (@Tpoint Tn) B'' T)))))))))))))) *)
assert (H1 : BetS B MB T) by (repeat split; Between).
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => @ex (@Tpoint Tn) (fun B'' : @Tpoint Tn => @ex (@Tpoint Tn) (fun MB : @Tpoint Tn => @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A B X) (and (@Par_strict Tn B C T X) (and (@BetS Tn B MB T) (and (@BetS Tn B' MB B'') (and (@Cong Tn B MB T MB) (and (@Cong Tn B' MB B'' MB) (and (@Col Tn B B' D) (and (@Bet Tn B'' T X) (and (not (@eq (@Tpoint Tn) B B')) (not (@eq (@Tpoint Tn) B'' T)))))))))))))) *)
assert (H2 : BetS B' MB B'') by (repeat split; Between).
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => @ex (@Tpoint Tn) (fun B'' : @Tpoint Tn => @ex (@Tpoint Tn) (fun MB : @Tpoint Tn => @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A B X) (and (@Par_strict Tn B C T X) (and (@BetS Tn B MB T) (and (@BetS Tn B' MB B'') (and (@Cong Tn B MB T MB) (and (@Cong Tn B' MB B'' MB) (and (@Col Tn B B' D) (and (@Bet Tn B'' T X) (and (not (@eq (@Tpoint Tn) B B')) (not (@eq (@Tpoint Tn) B'' T)))))))))))))) *)
assert (HB'T : B' <> T).
(* Goal: @OS Tn D A X B *)
  {
(* Goal: not (@eq (@Tpoint Tn) B' T) *)
  assert (H : ~ Col B B' T) by (intro; apply HABC; assert_cols; ColR).
(* Goal: not (@eq (@Tpoint Tn) B''' T) *)
  intro; treat_equalities; apply H; Col.
  }
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => @ex (@Tpoint Tn) (fun B'' : @Tpoint Tn => @ex (@Tpoint Tn) (fun MB : @Tpoint Tn => @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A B X) (and (@Par_strict Tn B C T X) (and (@BetS Tn B MB T) (and (@BetS Tn B' MB B'') (and (@Cong Tn B MB T MB) (and (@Cong Tn B' MB B'' MB) (and (@Col Tn B B' D) (and (@Bet Tn B'' T X) (and (not (@eq (@Tpoint Tn) B B')) (not (@eq (@Tpoint Tn) B'' T)))))))))))))) *)
assert (HB'B''' : B' <> B''').
(* Goal: @OS Tn D A X B *)
  {
(* Goal: not (@eq (@Tpoint Tn) B' B''') *)
  assert (H : ~ Col A B B') by (intro; apply HABC; assert_cols; ColR).
(* Goal: not (@eq (@Tpoint Tn) B''' T) *)
  intro; treat_equalities; apply H; Col.
  }
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => @ex (@Tpoint Tn) (fun B'' : @Tpoint Tn => @ex (@Tpoint Tn) (fun MB : @Tpoint Tn => @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A B X) (and (@Par_strict Tn B C T X) (and (@BetS Tn B MB T) (and (@BetS Tn B' MB B'') (and (@Cong Tn B MB T MB) (and (@Cong Tn B' MB B'' MB) (and (@Col Tn B B' D) (and (@Bet Tn B'' T X) (and (not (@eq (@Tpoint Tn) B B')) (not (@eq (@Tpoint Tn) B'' T)))))))))))))) *)
assert (HB'''T : B''' <> T).
(* Goal: @OS Tn D A X B *)
  {
(* Goal: not (@eq (@Tpoint Tn) B''' T) *)
  assert (H : ~ Col A B T) by (intro; apply HABC; assert_cols; ColR).
(* Goal: not (@eq (@Tpoint Tn) B''' T) *)
  intro; treat_equalities; apply H; Col.
  }
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => @ex (@Tpoint Tn) (fun B'' : @Tpoint Tn => @ex (@Tpoint Tn) (fun MB : @Tpoint Tn => @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A B X) (and (@Par_strict Tn B C T X) (and (@BetS Tn B MB T) (and (@BetS Tn B' MB B'') (and (@Cong Tn B MB T MB) (and (@Cong Tn B' MB B'' MB) (and (@Col Tn B B' D) (and (@Bet Tn B'' T X) (and (not (@eq (@Tpoint Tn) B B')) (not (@eq (@Tpoint Tn) B'' T)))))))))))))) *)
assert (H3 : BetS T B''' B') by (repeat split; Between).
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => @ex (@Tpoint Tn) (fun B'' : @Tpoint Tn => @ex (@Tpoint Tn) (fun MB : @Tpoint Tn => @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A B X) (and (@Par_strict Tn B C T X) (and (@BetS Tn B MB T) (and (@BetS Tn B' MB B'') (and (@Cong Tn B MB T MB) (and (@Cong Tn B' MB B'' MB) (and (@Col Tn B B' D) (and (@Bet Tn B'' T X) (and (not (@eq (@Tpoint Tn) B B')) (not (@eq (@Tpoint Tn) B'' T)))))))))))))) *)
assert (H4 : ~ Col B T B'') by (intro; apply HABC; assert_cols; ColR).
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => @ex (@Tpoint Tn) (fun B'' : @Tpoint Tn => @ex (@Tpoint Tn) (fun MB : @Tpoint Tn => @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A B X) (and (@Par_strict Tn B C T X) (and (@BetS Tn B MB T) (and (@BetS Tn B' MB B'') (and (@Cong Tn B MB T MB) (and (@Cong Tn B' MB B'' MB) (and (@Col Tn B B' D) (and (@Bet Tn B'' T X) (and (not (@eq (@Tpoint Tn) B B')) (not (@eq (@Tpoint Tn) B'' T)))))))))))))) *)
assert (H5 : Cong B MB T MB) by Cong.
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => @ex (@Tpoint Tn) (fun B'' : @Tpoint Tn => @ex (@Tpoint Tn) (fun MB : @Tpoint Tn => @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A B X) (and (@Par_strict Tn B C T X) (and (@BetS Tn B MB T) (and (@BetS Tn B' MB B'') (and (@Cong Tn B MB T MB) (and (@Cong Tn B' MB B'' MB) (and (@Col Tn B B' D) (and (@Bet Tn B'' T X) (and (not (@eq (@Tpoint Tn) B B')) (not (@eq (@Tpoint Tn) B'' T)))))))))))))) *)
assert (H6 : Cong B' MB B'' MB) by Cong.
destruct (HSPP B T B' B'' MB B''') as [X [HBetS HX]];
Col; Cop; try (intro; apply H4; assert_diffs; assert_cols; ColR).
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => @ex (@Tpoint Tn) (fun B'' : @Tpoint Tn => @ex (@Tpoint Tn) (fun MB : @Tpoint Tn => @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A B X) (and (@Par_strict Tn B C T X) (and (@BetS Tn B MB T) (and (@BetS Tn B' MB B'') (and (@Cong Tn B MB T MB) (and (@Cong Tn B' MB B'' MB) (and (@Col Tn B B' D) (and (@Bet Tn B'' T X) (and (not (@eq (@Tpoint Tn) B B')) (not (@eq (@Tpoint Tn) B'' T)))))))))))))) *)
assert (HNC : ~ Col B B' B''') by (intro; assert_diffs; assert_cols; apply H4; ColR).
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => @ex (@Tpoint Tn) (fun B'' : @Tpoint Tn => @ex (@Tpoint Tn) (fun MB : @Tpoint Tn => @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A B X) (and (@Par_strict Tn B C T X) (and (@BetS Tn B MB T) (and (@BetS Tn B' MB B'') (and (@Cong Tn B MB T MB) (and (@Cong Tn B' MB B'' MB) (and (@Col Tn B B' D) (and (@Bet Tn B'' T X) (and (not (@eq (@Tpoint Tn) B B')) (not (@eq (@Tpoint Tn) B'' T)))))))))))))) *)
assert (HPar1 : Par B B' T B'') by (unfold BetS in *; spliter; apply l12_17 with MB; try split; Col).
assert (HPar2 : Par B B'' T B')
  by (unfold BetS in *; spliter; assert_diffs; apply l12_17 with MB; try split; Between; Cong).
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => @ex (@Tpoint Tn) (fun B'' : @Tpoint Tn => @ex (@Tpoint Tn) (fun MB : @Tpoint Tn => @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A B X) (and (@Par_strict Tn B C T X) (and (@BetS Tn B MB T) (and (@BetS Tn B' MB B'') (and (@Cong Tn B MB T MB) (and (@Cong Tn B' MB B'' MB) (and (@Col Tn B B' D) (and (@Bet Tn B'' T X) (and (not (@eq (@Tpoint Tn) B B')) (not (@eq (@Tpoint Tn) B'' T)))))))))))))) *)
elim HBetS; clear HBetS; intro HBetS.

(* Goal: @OS Tn D A X B *)
  {
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => @ex (@Tpoint Tn) (fun B'' : @Tpoint Tn => @ex (@Tpoint Tn) (fun MB : @Tpoint Tn => @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A B X) (and (@Par_strict Tn B C T X) (and (@BetS Tn B MB T) (and (@BetS Tn B' MB B'') (and (@Cong Tn B MB T MB) (and (@Cong Tn B' MB B'' MB) (and (@Col Tn B B' D) (and (@Bet Tn B'' T X) (and (not (@eq (@Tpoint Tn) B B')) (not (@eq (@Tpoint Tn) B'' T)))))))))))))) *)
  elim HX; clear HX; intro HX.

(* Goal: @OS Tn D A X B *)
    {
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => @ex (@Tpoint Tn) (fun B'' : @Tpoint Tn => @ex (@Tpoint Tn) (fun MB : @Tpoint Tn => @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A B X) (and (@Par_strict Tn B C T X) (and (@BetS Tn B MB T) (and (@BetS Tn B' MB B'') (and (@Cong Tn B MB T MB) (and (@Cong Tn B' MB B'' MB) (and (@Col Tn B B' D) (and (@Bet Tn B'' T X) (and (not (@eq (@Tpoint Tn) B B')) (not (@eq (@Tpoint Tn) B'' T)))))))))))))) *)
    assert (H : BetS B'' T X).
(* Goal: @OS Tn D A X B *)
      {
(* Goal: @BetS Tn B'' T X *)
      repeat split; try (intro; treat_equalities); Col.
      apply H4; assert_diffs; assert_cols; ColR.
      }
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => @ex (@Tpoint Tn) (fun B'' : @Tpoint Tn => @ex (@Tpoint Tn) (fun MB : @Tpoint Tn => @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A B X) (and (@Par_strict Tn B C T X) (and (@BetS Tn B MB T) (and (@BetS Tn B' MB B'') (and (@Cong Tn B MB T MB) (and (@Cong Tn B' MB B'' MB) (and (@Col Tn B B' D) (and (@Bet Tn B'' T X) (and (not (@eq (@Tpoint Tn) B B')) (not (@eq (@Tpoint Tn) B'' T)))))))))))))) *)
    clear HBetS; rename H into HBetS.
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => @ex (@Tpoint Tn) (fun B'' : @Tpoint Tn => @ex (@Tpoint Tn) (fun MB : @Tpoint Tn => @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A B X) (and (@Par_strict Tn B C T X) (and (@BetS Tn B MB T) (and (@BetS Tn B' MB B'') (and (@Cong Tn B MB T MB) (and (@Cong Tn B' MB B'' MB) (and (@Col Tn B B' D) (and (@Bet Tn B'' T X) (and (not (@eq (@Tpoint Tn) B B')) (not (@eq (@Tpoint Tn) B'' T)))))))))))))) *)
    assert (H : BetS B B''' X).
(* Goal: @OS Tn D A X B *)
      {
      repeat split; try (intro; treat_equalities); Col; unfold BetS in *; spliter;
      apply H4; assert_diffs; assert_cols; ColR.
      }
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => @ex (@Tpoint Tn) (fun B'' : @Tpoint Tn => @ex (@Tpoint Tn) (fun MB : @Tpoint Tn => @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A B X) (and (@Par_strict Tn B C T X) (and (@BetS Tn B MB T) (and (@BetS Tn B' MB B'') (and (@Cong Tn B MB T MB) (and (@Cong Tn B' MB B'' MB) (and (@Col Tn B B' D) (and (@Bet Tn B'' T X) (and (not (@eq (@Tpoint Tn) B B')) (not (@eq (@Tpoint Tn) B'' T)))))))))))))) *)
    clear HX; rename H into HX.
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => @ex (@Tpoint Tn) (fun B'' : @Tpoint Tn => @ex (@Tpoint Tn) (fun MB : @Tpoint Tn => @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A B X) (and (@Par_strict Tn B C T X) (and (@BetS Tn B MB T) (and (@BetS Tn B' MB B'') (and (@Cong Tn B MB T MB) (and (@Cong Tn B' MB B'' MB) (and (@Col Tn B B' D) (and (@Bet Tn B'' T X) (and (not (@eq (@Tpoint Tn) B B')) (not (@eq (@Tpoint Tn) B'' T)))))))))))))) *)
    apply BetSEq in HBetS; destruct HBetS as [HB''TX [HB''T [HB''X HBTX]]].
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => @ex (@Tpoint Tn) (fun B'' : @Tpoint Tn => @ex (@Tpoint Tn) (fun MB : @Tpoint Tn => @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A B X) (and (@Par_strict Tn B C T X) (and (@BetS Tn B MB T) (and (@BetS Tn B' MB B'') (and (@Cong Tn B MB T MB) (and (@Cong Tn B' MB B'' MB) (and (@Col Tn B B' D) (and (@Bet Tn B'' T X) (and (not (@eq (@Tpoint Tn) B B')) (not (@eq (@Tpoint Tn) B'' T)))))))))))))) *)
    exists B'; exists B''; exists MB; exists X.
(* Goal: and (@Bet Tn A B X) (and (@Par_strict Tn B C T X) (and (@BetS Tn B MB T) (and (@BetS Tn B' MB B'') (and (@Cong Tn B MB T MB) (and (@Cong Tn B' MB B'' MB) (and (@Col Tn B B' D) (and (@Bet Tn B'' T X) (and (not (@eq (@Tpoint Tn) B B')) (not (@eq (@Tpoint Tn) B'' T)))))))))) *)
    split; unfold BetS in HX; spliter; eBetween.
(* Goal: and (@Par_strict Tn B C T X) (and (@BetS Tn B MB T) (and (@BetS Tn B' MB B'') (and (@Cong Tn B MB T MB) (and (@Cong Tn B' MB B'' MB) (and (@Col Tn B B' D) (and (@Bet Tn B'' T X) (and (not (@eq (@Tpoint Tn) B B')) (not (@eq (@Tpoint Tn) B'' T))))))))) *)
    assert (HPar : Par B' B B'' T) by (apply l12_17 with MB; try split; Between; Cong).
    assert (HPar' : Par B C B'' T)
      by (apply par_symmetry; apply par_col_par with B'; Par; assert_cols; ColR).
(* Goal: and (@Par_strict Tn B C T X) (and (@BetS Tn B MB T) (and (@BetS Tn B' MB B'') (and (@Cong Tn B MB T MB) (and (@Cong Tn B' MB B'' MB) (and (@Col Tn B B' D) (and (@Bet Tn B'' T X) (and (not (@eq (@Tpoint Tn) B B')) (not (@eq (@Tpoint Tn) B'' T))))))))) *)
    split.

(* Goal: @OS Tn D A X B *)
      {
(* Goal: @Par_strict Tn B C T X *)
      apply par_not_col_strict with T; Col.

(* Goal: @OS Tn D A X B *)
        {
(* Goal: @Par Tn B C T X *)
        apply par_col_par with B''; Par.
        assert_cols; ColR.
        }

(* Goal: @OS Tn D A X B *)
        {
        intro; apply HABC; assert_cols; ColR.
        }
      }

(* Goal: @OS Tn D A X B *)
      {
(* Goal: and (@BetS Tn B MB T) (and (@BetS Tn B' MB B'') (and (@Cong Tn B MB T MB) (and (@Cong Tn B' MB B'' MB) (and (@Col Tn B B' D) (and (@Bet Tn B'' T X) (and (not (@eq (@Tpoint Tn) B B')) (not (@eq (@Tpoint Tn) B'' T)))))))) *)
      repeat (split; try assumption); unfold BetS in *; spliter; assert_cols; Col.
      }
    }

(* Goal: @OS Tn D A X B *)
    {
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => @ex (@Tpoint Tn) (fun B'' : @Tpoint Tn => @ex (@Tpoint Tn) (fun MB : @Tpoint Tn => @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A B X) (and (@Par_strict Tn B C T X) (and (@BetS Tn B MB T) (and (@BetS Tn B' MB B'') (and (@Cong Tn B MB T MB) (and (@Cong Tn B' MB B'' MB) (and (@Col Tn B B' D) (and (@Bet Tn B'' T X) (and (not (@eq (@Tpoint Tn) B B')) (not (@eq (@Tpoint Tn) B'' T)))))))))))))) *)
    elim HX; clear HX; intro HX.

(* Goal: @OS Tn D A X B *)
      {
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => @ex (@Tpoint Tn) (fun B'' : @Tpoint Tn => @ex (@Tpoint Tn) (fun MB : @Tpoint Tn => @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A B X) (and (@Par_strict Tn B C T X) (and (@BetS Tn B MB T) (and (@BetS Tn B' MB B'') (and (@Cong Tn B MB T MB) (and (@Cong Tn B' MB B'' MB) (and (@Col Tn B B' D) (and (@Bet Tn B'' T X) (and (not (@eq (@Tpoint Tn) B B')) (not (@eq (@Tpoint Tn) B'' T)))))))))))))) *)
      exfalso; apply impossible_case_5 with B T B' B'' MB B''' X; spliter; assumption.
      }

(* Goal: @OS Tn D A X B *)
      {
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => @ex (@Tpoint Tn) (fun B'' : @Tpoint Tn => @ex (@Tpoint Tn) (fun MB : @Tpoint Tn => @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A B X) (and (@Par_strict Tn B C T X) (and (@BetS Tn B MB T) (and (@BetS Tn B' MB B'') (and (@Cong Tn B MB T MB) (and (@Cong Tn B' MB B'' MB) (and (@Col Tn B B' D) (and (@Bet Tn B'' T X) (and (not (@eq (@Tpoint Tn) B B')) (not (@eq (@Tpoint Tn) B'' T)))))))))))))) *)
      exfalso; apply impossible_case_6 with B T B' B'' MB B''' X; spliter; assumption.
      }
    }
  }

(* Goal: @OS Tn D A X B *)
  {
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => @ex (@Tpoint Tn) (fun B'' : @Tpoint Tn => @ex (@Tpoint Tn) (fun MB : @Tpoint Tn => @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A B X) (and (@Par_strict Tn B C T X) (and (@BetS Tn B MB T) (and (@BetS Tn B' MB B'') (and (@Cong Tn B MB T MB) (and (@Cong Tn B' MB B'' MB) (and (@Col Tn B B' D) (and (@Bet Tn B'' T X) (and (not (@eq (@Tpoint Tn) B B')) (not (@eq (@Tpoint Tn) B'' T)))))))))))))) *)
  elim HBetS; clear HBetS; intro HBetS.

(* Goal: @OS Tn D A X B *)
    {
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => @ex (@Tpoint Tn) (fun B'' : @Tpoint Tn => @ex (@Tpoint Tn) (fun MB : @Tpoint Tn => @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A B X) (and (@Par_strict Tn B C T X) (and (@BetS Tn B MB T) (and (@BetS Tn B' MB B'') (and (@Cong Tn B MB T MB) (and (@Cong Tn B' MB B'' MB) (and (@Col Tn B B' D) (and (@Bet Tn B'' T X) (and (not (@eq (@Tpoint Tn) B B')) (not (@eq (@Tpoint Tn) B'' T)))))))))))))) *)
    exfalso; apply impossible_case_7 with B T B' B'' MB B''' X; spliter; assumption.
    }

(* Goal: @OS Tn D A X B *)
    {
(* Goal: @ex (@Tpoint Tn) (fun B' : @Tpoint Tn => @ex (@Tpoint Tn) (fun B'' : @Tpoint Tn => @ex (@Tpoint Tn) (fun MB : @Tpoint Tn => @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Bet Tn A B X) (and (@Par_strict Tn B C T X) (and (@BetS Tn B MB T) (and (@BetS Tn B' MB B'') (and (@Cong Tn B MB T MB) (and (@Cong Tn B' MB B'' MB) (and (@Col Tn B B' D) (and (@Bet Tn B'' T X) (and (not (@eq (@Tpoint Tn) B B')) (not (@eq (@Tpoint Tn) B'' T)))))))))))))) *)
    exfalso; apply impossible_case_8 with B T B' B'' MB B''' X; spliter; assumption.
    }
  }

Qed.

Lemma strong_parallel_postulate_implies_tarski_s_euclid :
  strong_parallel_postulate ->
  tarski_s_parallel_postulate.
Proof.
(* Goal: forall _ : @strong_parallel_postulate Tn, @tarski_s_parallel_postulate Tn *)
unfold tarski_s_parallel_postulate.
(* Goal: forall (_ : @strong_parallel_postulate Tn) (A B C D T : @Tpoint Tn) (_ : @Bet Tn A D T) (_ : @Bet Tn B D C) (_ : not (@eq (@Tpoint Tn) A D)), @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Bet Tn A B X) (and (@Bet Tn A C Y) (@Bet Tn X T Y)))) *)
intro HSPP; apply tarski_s_euclid_remove_degenerated_cases.
(* Goal: forall (A B C D T : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : not (@eq (@Tpoint Tn) A C)) (_ : not (@eq (@Tpoint Tn) A D)) (_ : not (@eq (@Tpoint Tn) A T)) (_ : not (@eq (@Tpoint Tn) B C)) (_ : not (@eq (@Tpoint Tn) B D)) (_ : not (@eq (@Tpoint Tn) B T)) (_ : not (@eq (@Tpoint Tn) C D)) (_ : not (@eq (@Tpoint Tn) C T)) (_ : not (@eq (@Tpoint Tn) D T)) (_ : not (@Col Tn A B C)) (_ : @Bet Tn A D T) (_ : @Bet Tn B D C), @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
intros A B C D T HAB HAC HAD HAT HBC HBD HBT HCD HCT HDT HABC HADT HBDC.
destruct (strong_parallel_postulate_implies_tarski_s_euclid_aux HSPP A B C D T)
as [B' [B'' [MB [X [HABX [HPar' [HBet1 [HBet2 [HCong1 [HCong2 [HBB'D [HB''TX [HBB' HB''T]]]]]]]]]]]]];
destruct (strong_parallel_postulate_implies_tarski_s_euclid_aux HSPP A C B D T)
as [C' [C'' [MC [Y [HACY [HPar [HBet3 [HBet4 [HCong3 [HCong4 [HCC'D [HC''TY [HCC' HC''T]]]]]]]]]]]]];
Between; Col.
clear HBet3; clear HBet4; clear HCong3; clear HCong4;
clear MC; clear HC''TY; clear HC''T; clear HPar'.
(* Goal: @ex (@Tpoint Tn) (fun x : @Tpoint Tn => @ex (@Tpoint Tn) (fun y : @Tpoint Tn => and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)))) *)
exists X; exists Y; repeat split; try assumption.
(* Goal: @Bet Tn X T Y *)
elim (col_dec X T Y); intro HXTY.

(* Goal: @OS Tn D A X B *)
  {
(* Goal: @Bet Tn X T Y *)
  apply between_symmetry in HACY.
(* Goal: @Bet Tn X T Y *)
  assert (HU := outer_pasch Y B C A D HACY HBDC); destruct HU as [U [HYUB HADU]].
(* Goal: @Bet Tn X T Y *)
  apply between_symmetry in HABX.
(* Goal: @Bet Tn X T Y *)
  assert (HV := outer_pasch X Y B A U HABX HYUB); destruct HV as [V [HXVY HAUV]].
(* Goal: @Bet Tn X T Y *)
  assert (HAX : A <> X) by (intro; treat_equalities; Col).
(* Goal: @Bet Tn X T Y *)
  assert (HAY : A <> Y) by (intro; treat_equalities; Col).
(* Goal: @Bet Tn X T Y *)
  assert (HAXY : ~ Col A X Y) by (intro; assert_cols; apply HABC; ColR).
(* Goal: @Bet Tn X T Y *)
  assert (HAU : A <> U) by (intro; treat_equalities; Col).
(* Goal: @Bet Tn X T Y *)
  assert (HEq : T = V) by (assert_cols; apply l6_21 with X Y A D; Col; ColR); subst; assumption.
  }

(* Goal: @OS Tn D A X B *)
  {
(* Goal: @Bet Tn X T Y *)
  assert (HNC : ~ Col T B'' Y) by (intro; apply HXTY; unfold BetS in *; spliter; assert_cols; ColR).
(* Goal: @Bet Tn X T Y *)
  assert (HCop : Coplanar T B B'' Y).
(* Goal: @OS Tn D A X B *)
    {
(* Goal: @Coplanar Tn T B B'' Y *)
    apply coplanar_pseudo_trans with A B C; assert_cols; Cop.

(* Goal: @OS Tn D A X B *)
      {
(* Goal: @Coplanar Tn A B C T *)
      exists D; assert_cols; Col5.
      }

(* Goal: @OS Tn D A X B *)
      {
(* Goal: @Coplanar Tn A B C B'' *)
      assert (HABD : ~ Col D A B) by (intro; assert_cols; apply HABC; ColR).
(* Goal: @Coplanar Tn A B C B'' *)
      apply coplanar_trans_1 with D; [Cop..|].
(* Goal: @Coplanar Tn D A B B'' *)
      apply ts__coplanar.
(* Goal: @TS Tn D A B B'' *)
      apply l9_8_2 with X.

(* Goal: @OS Tn D A X B *)
        {
(* Goal: and (@Out Tn A X B) (not (@Col Tn A D X)) *)
        assert (HAX : A <> X) by (intro; treat_equalities; apply HABC; Col).
(* Goal: and (not (@Col Tn B'' D A)) (@ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T D A) (@Bet Tn X T B''))) *)
        split; try (intro; assert_cols; apply HABC; ColR).
(* Goal: and (not (@Col Tn B'' D A)) (@ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T D A) (@Bet Tn X T B''))) *)
        split; try (intro; assert_cols; apply HABC; ColR).
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T D A) (@Bet Tn X T B'')) *)
        exists T; split; Col; Between.
        }

(* Goal: @OS Tn D A X B *)
        {
(* Goal: @OS Tn D A X B *)
        apply invert_one_side.
(* Goal: @OS Tn A D X B *)
        assert (HADA : Col A D A) by Col.
(* Goal: @OS Tn A D X B *)
        assert (HXBA : Col X B A) by (assert_cols; Col).
(* Goal: @OS Tn A D X B *)
        rewrite (l9_19 A D X B A HADA HXBA).
(* Goal: and (@Out Tn A X B) (not (@Col Tn A D X)) *)
        assert (HAX : A <> X) by (intro; treat_equalities; apply HABC; Col).
(* Goal: and (@Out Tn A X B) (not (@Col Tn A D X)) *)
        split; try (intro; assert_cols; apply HABC; ColR); split; auto.
        }
      }
    }
  destruct (HSPP T B B'' B' MB Y) as [I [HCol1 HCol2]]; Cong;
  try (unfold BetS in *; spliter; repeat (split; try Between)).
(* Goal: @Bet Tn X T Y *)
  exfalso; apply HPar; exists I; split; Col.
(* Goal: @Col Tn I C B *)
  elim (eq_dec_points I B); intro HBI; subst; Col.
  unfold BetS in *; spliter; assert_cols; ColR.
  }
Qed.

End SPP_tarski.