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

Section TCP_tarski.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma impossible_case_1 :
  forall A B C D T x y,
  A <> B ->
  A <> C ->
  A <> D ->
  A <> T ->
  B <> C ->
  B <> D ->
  B <> T ->
  C <> D ->
  C <> T ->
  D <> T ->
  x <> y ->
  ~ Col A B C ->
  Bet A D T ->
  ~ Col B C T ->
  Bet B D C ->
  Bet A B x ->
  Bet C y A ->
  Bet x T y ->
  Par_strict B C x y ->
  False.
Proof.
(* Goal: forall (A B C D T x y : @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 (@eq (@Tpoint Tn) x y)) (_ : not (@Col Tn A B C)) (_ : @Col Tn A C y) (_ : @Bet Tn A D T) (_ : not (@Col Tn B C T)) (_ : @Bet Tn B D C) (_ : @Col Tn A B x) (_ : @Bet Tn T y x) (_ : @Par_strict Tn B C x y), False *)
intros A B C D T x y.
(* Goal: forall (_ : 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 (@eq (@Tpoint Tn) x y)) (_ : not (@Col Tn A B C)) (_ : @Col Tn A C y) (_ : @Bet Tn A D T) (_ : not (@Col Tn B C T)) (_ : @Bet Tn B D C) (_ : @Col Tn A B x) (_ : @Bet Tn T y x) (_ : @Par_strict Tn B C x y), False *)
intros HAB HAC HAD HAT HBC HBD HBT HCD HCT HDT Hxy.
(* Goal: forall (_ : not (@Col Tn A B C)) (_ : @Bet Tn A D T) (_ : not (@Col Tn B C T)) (_ : @Bet Tn B D C) (_ : @Bet Tn A B x) (_ : @Bet Tn C y A) (_ : @Bet Tn x T y) (_ : @Par_strict Tn B C x y), False *)
intros HABC HADT HBCT HBDC HABx HACy HxTy HPar.
(* Goal: False *)
apply between_symmetry in HABx.
(* Goal: False *)
assert (HI := inner_pasch x C A B y HABx HACy); destruct HI as [I [HBCI HIxy]].
(* Goal: False *)
apply HPar; exists I; assert_cols; Col.
Qed.

Lemma impossible_case_2 :
  forall A B C D T x y,
  A <> B ->
  A <> C ->
  A <> D ->
  A <> T ->
  B <> C ->
  B <> D ->
  B <> T ->
  C <> D ->
  C <> T ->
  D <> T ->
  x <> y ->
  ~ Col A B C ->
  Col A B x ->
  Bet A D T ->
  ~ Col B C T ->
  Bet B D C ->
  Bet y A C ->
  Bet x T y ->
  False.
Proof.
(* Goal: forall (A B C D T x y : @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 (@eq (@Tpoint Tn) x y)) (_ : not (@Col Tn A B C)) (_ : @Col Tn A C y) (_ : @Bet Tn A D T) (_ : not (@Col Tn B C T)) (_ : @Bet Tn B D C) (_ : @Col Tn A B x) (_ : @Bet Tn T y x) (_ : @Par_strict Tn B C x y), False *)
intros A B C D T x y.
(* Goal: forall (_ : 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 (@eq (@Tpoint Tn) x y)) (_ : not (@Col Tn A B C)) (_ : @Col Tn A C y) (_ : @Bet Tn A D T) (_ : not (@Col Tn B C T)) (_ : @Bet Tn B D C) (_ : @Col Tn A B x) (_ : @Bet Tn T y x) (_ : @Par_strict Tn B C x y), False *)
intros HAB HAC HAD HAT HBC HBD HBT HCD HCT HDT Hxy.
(* Goal: forall (_ : not (@Col Tn A B C)) (_ : @Col Tn A B x) (_ : @Bet Tn A D T) (_ : not (@Col Tn B C T)) (_ : @Bet Tn B D C) (_ : @Bet Tn y A C) (_ : @Bet Tn x T y), False *)
intros HABC HABx HADT HBCT HBDC HACy HxTy.
(* Goal: False *)
apply between_symmetry in HACy.
(* Goal: False *)
assert (HI := inner_pasch C x y A T HACy HxTy); destruct HI as [I [HAIx HICT]].
(* Goal: False *)
assert (HAx : A <> x) by (intro; treat_equalities; apply HABC; assert_cols; ColR).
assert (HTS : TS A B C T) by (repeat (split; Col); try (intro; apply HBCT; assert_cols; ColR);
exists I; split; Between; assert_cols; ColR); apply l9_9 in HTS.
(* Goal: False *)
apply HTS; apply one_side_transitivity with D.

(* Goal: @OS Tn A B C D *)
(* Goal: @OS Tn A B D T *)
  assert (HABB : Col A B B) by Col.
(* Goal: @OS Tn A B C D *)
(* Goal: @OS Tn A B D T *)
  assert (HBDC' : Col C D B) by (assert_cols; Col).
(* Goal: @OS Tn A B C D *)
(* Goal: @OS Tn A B D T *)
  assert (H := l9_19 A B C D B HABB HBDC'); rewrite H.
(* Goal: and (@Out Tn C B D) (not (@Col Tn A C B)) *)
(* Goal: @OS Tn A C D T *)
  split; try (intro; apply HABC; Col).
(* Goal: @Out Tn A D T *)
  repeat (split; Between).

(* Goal: @OS Tn A B D T *)
  assert (HABA : Col A B A) by Col.
(* Goal: @OS Tn A C D T *)
  assert (HDTA : Col D T A) by (assert_cols; Col).
(* Goal: @OS Tn A B D T *)
  assert (H := l9_19 A B D T A HABA HDTA); rewrite H.
(* Goal: and (@Out Tn A D T) (not (@Col Tn A C D)) *)
  split; try (intro; apply HABC; assert_cols; ColR).
(* Goal: @Out Tn A D T *)
  repeat (split; Between).
Qed.

Lemma impossible_case_3 :
  forall A B C D T x y,
  A <> B ->
  A <> C ->
  A <> D ->
  A <> T ->
  B <> C ->
  B <> D ->
  B <> T ->
  C <> D ->
  C <> T ->
  D <> T ->
  x <> y ->
  ~ Col A B C ->
  Bet A D T ->
  ~ Col B C T ->
  Bet B D C ->
  Bet B x A ->
  Bet x T y ->
  Par_strict B C x y ->
  False.
Proof.
(* Goal: forall (A B C D T x y : @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 (@eq (@Tpoint Tn) x y)) (_ : not (@Col Tn A B C)) (_ : @Col Tn A C y) (_ : @Bet Tn A D T) (_ : not (@Col Tn B C T)) (_ : @Bet Tn B D C) (_ : @Col Tn A B x) (_ : @Bet Tn T y x) (_ : @Par_strict Tn B C x y), False *)
intros A B C D T x y.
(* Goal: forall (_ : 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 (@eq (@Tpoint Tn) x y)) (_ : not (@Col Tn A B C)) (_ : @Col Tn A C y) (_ : @Bet Tn A D T) (_ : not (@Col Tn B C T)) (_ : @Bet Tn B D C) (_ : @Col Tn A B x) (_ : @Bet Tn T y x) (_ : @Par_strict Tn B C x y), False *)
intros HAB HAC HAD HAT HBC HBD HBT HCD HCT HDT Hxy.
(* Goal: forall (_ : not (@Col Tn A B C)) (_ : @Bet Tn A D T) (_ : not (@Col Tn B C T)) (_ : @Bet Tn B D C) (_ : @Bet Tn B x A) (_ : @Bet Tn x T y) (_ : @Par_strict Tn B C x y), False *)
intros HABC HADT HBCT HBDC HABx HxTy HPar.
(* Goal: False *)
apply between_symmetry in HADT.
(* Goal: False *)
assert (HI := inner_pasch B T A x D HABx HADT); destruct HI as [I [HITx HBDI]].
(* Goal: False *)
assert (HTx : T <> x) by (intro; subst; apply HABC; assert_cols; ColR).
assert (HPar' : Par_strict B D x T) by (apply par_strict_col_par_strict with y; assert_cols; Col;
apply par_strict_symmetry; apply par_strict_col_par_strict with C; Col; Par).
(* Goal: False *)
apply HPar'; exists I; assert_cols; Col.
Qed.

Lemma impossible_case_4_1 :
  forall A B C D T x y,
  A <> B ->
  A <> C ->
  A <> D ->
  A <> T ->
  B <> C ->
  B <> D ->
  B <> T ->
  C <> D ->
  C <> T ->
  D <> T ->
  x <> y ->
  ~ Col A B C ->
  Col A C y ->
  Bet A D T ->
  ~ Col B C T ->
  Bet B D C ->
  Bet A x B \/ Bet A B x ->
  Bet T y x ->
  False.
Proof.
(* Goal: forall (A B C D T x y : @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 (@eq (@Tpoint Tn) x y)) (_ : not (@Col Tn A B C)) (_ : @Col Tn A C y) (_ : @Bet Tn A D T) (_ : not (@Col Tn B C T)) (_ : @Bet Tn B D C) (_ : @Col Tn A B x) (_ : @Bet Tn T y x) (_ : @Par_strict Tn B C x y), False *)
intros A B C D T x y.
(* Goal: forall (_ : 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 (@eq (@Tpoint Tn) x y)) (_ : not (@Col Tn A B C)) (_ : @Col Tn A C y) (_ : @Bet Tn A D T) (_ : not (@Col Tn B C T)) (_ : @Bet Tn B D C) (_ : @Col Tn A B x) (_ : @Bet Tn T y x) (_ : @Par_strict Tn B C x y), False *)
intros HAB HAC HAD HAT HBC HBD HBT HCD HCT HDT Hxy.
(* Goal: forall (_ : not (@Col Tn A B C)) (_ : @Col Tn A C y) (_ : @Bet Tn A D T) (_ : not (@Col Tn B C T)) (_ : @Bet Tn B D C) (_ : or (@Bet Tn A x B) (@Bet Tn A B x)) (_ : @Bet Tn T y x), False *)
intros HABC HACy HADT HBCT HBDC HABx HTyx.
assert (HTS : TS A C x T) by (repeat (split; Col); try (intro; apply HBCT; assert_cols; ColR);
                                     exists y; split; assert_cols; Col; Between).
(* Goal: False *)
assert (HAx : A <> x) by (intro; subst; apply HABC; assert_cols; ColR).
(* Goal: False *)
assert (HOS : OS A C x B).
(* Goal: @Par Tn B C x y *)
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
{
(* Goal: @OS Tn A C D T *)
  assert (HACA : Col A C A) by Col.
(* Goal: @OS Tn A C x B *)
  assert (HABx' : Col x B A) by (induction HABx; assert_cols; Col).
(* Goal: @OS Tn A C x B *)
  assert (H := l9_19 A C x B A HACA HABx'); rewrite H.
(* Goal: and (@Out Tn A D T) (not (@Col Tn A C D)) *)
  split; try (intro; apply HABC; assert_cols; ColR).
(* Goal: @Out Tn A x B *)
  repeat (split; auto).
}
assert (HTS' : TS A C B T) by (apply l9_8_2 with x; assumption);
clear HTS; clear HOS; rename HTS' into HTS; apply l9_9 in HTS.
(* Goal: False *)
apply HTS; apply one_side_transitivity with D.

(* Goal: @OS Tn A C B D *)
(* Goal: @OS Tn A C D T *)
  assert (HACC : Col A C C) by Col.
(* Goal: @OS Tn A C B D *)
(* Goal: @OS Tn A C D T *)
  assert (HBDC' : Col B D C) by (assert_cols; Col).
(* Goal: @OS Tn A C B D *)
(* Goal: @OS Tn A C D T *)
  assert (H := l9_19 A C B D C HACC HBDC'); rewrite H.
(* Goal: and (@Out Tn C B D) (not (@Col Tn A C B)) *)
(* Goal: @OS Tn A C D T *)
  split; try (intro; apply HABC; Col).
(* Goal: @Out Tn A D T *)
  repeat (split; Between).

(* Goal: @OS Tn A C D T *)
  assert (HACA : Col A C A) by Col.
(* Goal: @OS Tn A C D T *)
  assert (HDTA : Col D T A) by (assert_cols; Col).
(* Goal: @OS Tn A C D T *)
  assert (H := l9_19 A C D T A HACA HDTA); rewrite H.
(* Goal: and (@Out Tn A D T) (not (@Col Tn A C D)) *)
  split; try (intro; apply HABC; assert_cols; ColR).
(* Goal: @Out Tn A D T *)
  repeat (split; Between).
Qed.

Lemma impossible_case_4_2 :
  forall A B C D T x y,
  A <> B ->
  A <> C ->
  A <> D ->
  A <> T ->
  B <> C ->
  B <> D ->
  B <> T ->
  C <> D ->
  C <> T ->
  D <> T ->
  x <> y ->
  ~ Col A B C ->
  Col A C y ->
  Bet A D T ->
  ~ Col B C T ->
  Bet B D C ->
  Bet B A x ->
  Bet T y x ->
  Par_strict B C x y ->
  False.
Proof.
(* Goal: forall (A B C D T x y : @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 (@eq (@Tpoint Tn) x y)) (_ : not (@Col Tn A B C)) (_ : @Col Tn A C y) (_ : @Bet Tn A D T) (_ : not (@Col Tn B C T)) (_ : @Bet Tn B D C) (_ : @Col Tn A B x) (_ : @Bet Tn T y x) (_ : @Par_strict Tn B C x y), False *)
intros A B C D T x y.
(* Goal: forall (_ : 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 (@eq (@Tpoint Tn) x y)) (_ : not (@Col Tn A B C)) (_ : @Col Tn A C y) (_ : @Bet Tn A D T) (_ : not (@Col Tn B C T)) (_ : @Bet Tn B D C) (_ : @Col Tn A B x) (_ : @Bet Tn T y x) (_ : @Par_strict Tn B C x y), False *)
intros HAB HAC HAD HAT HBC HBD HBT HCD HCT HDT Hxy.
(* Goal: forall (_ : not (@Col Tn A B C)) (_ : @Col Tn A C y) (_ : @Bet Tn A D T) (_ : not (@Col Tn B C T)) (_ : @Bet Tn B D C) (_ : @Col Tn A B x) (_ : @Bet Tn T y x) (_ : @Par_strict Tn B C x y), False *)
intros HABC HACy HADT HBCT HBDC HABx HTyx HPar.
assert (HTS : TS B C A T) by (repeat (split; Col); try (intro; apply HBCT; assert_cols; ColR);
                                     exists D; split; assert_cols; Col; Between).
(* Goal: False *)
assert (HOS : OS B C A x).
(* Goal: @Par Tn B C x y *)
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
{
(* Goal: @OS Tn B C A x *)
  assert (HBCB : Col B C B) by Col.
(* Goal: @OS Tn B C A x *)
  assert (HABx' : Col A x B) by Col.
(* Goal: @OS Tn B C A x *)
  assert (H := l9_19 B C A x B HBCB HABx'); rewrite H.
(* Goal: and (@Out Tn A D T) (not (@Col Tn A C D)) *)
  split; try (intro; apply HABC; assert_cols; ColR).
(* Goal: @Out Tn A D T *)
  repeat (split; Between).
(* Goal: not (@eq (@Tpoint Tn) x B) *)
  intro; treat_equalities; intuition.
}
assert (HTS' : TS B C x T) by (apply l9_8_2 with A; assumption);
clear HTS; clear HOS; destruct HTS' as [Hclear [Hclear' [I [HBCI HITx]]]];
clear Hclear; clear Hclear'.
(* Goal: False *)
assert (HTx : T <> x) by (intro; subst; apply HABC; assert_cols; ColR).
(* Goal: False *)
assert (HPar' : Par_strict B C x T) by (apply par_strict_col_par_strict with y; assert_cols; Col).
(* Goal: False *)
apply HPar'; exists I; assert_cols; Col.
Qed.

Lemma impossible_case_4 :
  forall A B C D T x y,
  A <> B ->
  A <> C ->
  A <> D ->
  A <> T ->
  B <> C ->
  B <> D ->
  B <> T ->
  C <> D ->
  C <> T ->
  D <> T ->
  x <> y ->
  ~ Col A B C ->
  Col A C y ->
  Bet A D T ->
  ~ Col B C T ->
  Bet B D C ->
  Col A B x ->
  Bet T y x ->
  Par_strict B C x y ->
  False.
Proof.
(* Goal: forall (A B C D T x y : @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 (@eq (@Tpoint Tn) x y)) (_ : not (@Col Tn A B C)) (_ : @Col Tn A C y) (_ : @Bet Tn A D T) (_ : not (@Col Tn B C T)) (_ : @Bet Tn B D C) (_ : @Col Tn A B x) (_ : @Bet Tn T y x) (_ : @Par_strict Tn B C x y), False *)
intros A B C D T x y.
(* Goal: forall (_ : 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 (@eq (@Tpoint Tn) x y)) (_ : not (@Col Tn A B C)) (_ : @Col Tn A C y) (_ : @Bet Tn A D T) (_ : not (@Col Tn B C T)) (_ : @Bet Tn B D C) (_ : @Col Tn A B x) (_ : @Bet Tn T y x) (_ : @Par_strict Tn B C x y), False *)
intros HAB HAC HAD HAT HBC HBD HBT HCD HCT HDT Hxy.
(* Goal: forall (_ : not (@Col Tn A B C)) (_ : @Col Tn A C y) (_ : @Bet Tn A D T) (_ : not (@Col Tn B C T)) (_ : @Bet Tn B D C) (_ : @Col Tn A B x) (_ : @Bet Tn T y x) (_ : @Par_strict Tn B C x y), False *)
intros HABC HACy HADT HBCT HBDC HABx HTyx HPar.
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
elim HABx; clear HABx; intro HABx.

(* Goal: False *)
(* Goal: False *)
  apply impossible_case_4_1 with A B C D T x y; Col.

(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
  elim HABx; clear HABx; intro HABx.

(* Goal: False *)
(* Goal: False *)
    apply impossible_case_4_1 with A B C D T x y; Between.

(* Goal: False *)
    apply impossible_case_4_2 with A B C D T x y; Between.
Qed.

Lemma impossible_two_sides_not_col : forall A B C D T Y,
  A <> B ->
  A <> C ->
  A <> D ->
  A <> T ->
  A <> Y ->
  B <> C ->
  B <> D ->
  B <> T ->
  B <> Y ->
  C <> D ->
  C <> T ->
  C <> Y ->
  D <> T ->
  T <> Y ->
  ~ Col A B C ->
  Bet A D T ->
  ~ Col B C T ->
  Bet B D C ->
  Bet B Y T ->
  ~ Col A C Y.
Proof.
(* Goal: forall (A B C D T Y : @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) A Y)) (_ : not (@eq (@Tpoint Tn) B C)) (_ : not (@eq (@Tpoint Tn) B D)) (_ : not (@eq (@Tpoint Tn) B T)) (_ : not (@eq (@Tpoint Tn) B Y)) (_ : not (@eq (@Tpoint Tn) C D)) (_ : not (@eq (@Tpoint Tn) C T)) (_ : not (@eq (@Tpoint Tn) C Y)) (_ : not (@eq (@Tpoint Tn) D T)) (_ : not (@eq (@Tpoint Tn) T Y)) (_ : not (@Col Tn A B C)) (_ : @Bet Tn A D T) (_ : not (@Col Tn B C T)) (_ : @Bet Tn B D C) (_ : @Bet Tn B Y T), not (@Col Tn A C Y) *)
intros A B C D T Y HAB HAC HAD HAT HAY HBC HBD HBT HBY HCD HCT HCY HDT HTY.
intros  HABC HADT HBCT HBDC HBYT.
(* Goal: not (@Col Tn A C Y) *)
intro HACY.
assert (HTS : TS A C B T)
  by (repeat (split; Col); try (intro; apply HABC; assert_cols; ColR); exists Y; split; Col; Between).
(* Goal: False *)
apply l9_9 in HTS; apply HTS; apply one_side_transitivity with D.

(* Goal: @OS Tn A C B D *)
(* Goal: @OS Tn A C D T *)
  assert (HACC : Col A C C) by Col.
(* Goal: @OS Tn A C B D *)
(* Goal: @OS Tn A C D T *)
  assert (HBDC' : Col B D C) by (assert_cols; Col).
(* Goal: @OS Tn A C B D *)
(* Goal: @OS Tn A C D T *)
  assert (H := l9_19 A C B D C HACC HBDC'); rewrite H.
(* Goal: and (@Out Tn C B D) (not (@Col Tn A C B)) *)
(* Goal: @OS Tn A C D T *)
  split; try (intro; apply HABC; Col).
(* Goal: @Out Tn A D T *)
  repeat (split; Between).

(* Goal: @OS Tn A C D T *)
  assert (HACA : Col A C A) by Col.
(* Goal: @OS Tn A C D T *)
  assert (HDTA : Col D T A) by (assert_cols; Col).
(* Goal: @OS Tn A C D T *)
  assert (H := l9_19 A C D T A HACA HDTA); rewrite H.
(* Goal: and (@Out Tn A D T) (not (@Col Tn A C D)) *)
  split; try (intro; apply HABC; assert_cols; ColR).
(* Goal: @Out Tn A D T *)
  repeat (split; Between).
Qed.

(*
Lemma triangle_circumscription_aux : forall A B C P,
  Cong A P B P -> Cong A P C P -> exists CC, Cong A CC B CC /\ Cong A CC C CC /\ Coplanar A B C CC.
Proof.
  intros A B C D HCong1 HCong2.
  destruct (cop_dec A B C D).
    exists D; repeat split; assumption.
  destruct (l11_62_existence A B C D) as [CC [HCop HCC]].
  exists CC.
  assert (CC <> D) by (intro; subst; Cop).
(* Goal: @Coplanar Tn Y Z1 B A *)
(* Goal: @Coplanar Tn Y Z1 B C *)
(* Goal: @Perp Tn A C Y Z1 *)
(* 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)))) *)
(* 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)))) *)
(* 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)))) *)
  assert (Per B CC D) by Cop.
  assert (A <> CC).
(* Goal: @Par Tn B C x y *)
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
  { intro; subst CC.
    destruct (l11_46 B A D) as [_ []]; auto.
    assert_diffs; apply per_not_col; auto.
  }
(* Goal: @Coplanar Tn Y Z1 B A *)
(* Goal: @Coplanar Tn Y Z1 B C *)
(* Goal: @Perp Tn A C Y Z1 *)
(* 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)))) *)
(* 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)))) *)
(* 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)))) *)
  assert (Per A CC D) by Cop.
  repeat split; trivial.
  - destruct (cong2_per2__cong_conga2 A CC D B CC D); Cong.
    intro; subst CC.
    destruct (l11_46 A B D) as [_ []]; Cong.
    assert_diffs; apply per_not_col; auto.
(* Goal: @Coplanar Tn Y Z1 B A *)
(* Goal: @Coplanar Tn Y Z1 B C *)
(* Goal: @Perp Tn A C Y Z1 *)
(* 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)))) *)
(* 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)))) *)
(* 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)))) *)
  - assert (Per C CC D) by Cop.
    destruct (cong2_per2__cong_conga2 A CC D C CC D); Cong.
    intro; subst CC.
    destruct (l11_46 A C D) as [_ []]; Cong.
    apply per_not_col; auto.
Qed.
*)

Lemma triangle_circumscription_implies_tarski_s_euclid_aux :
  forall A B C D T X Y Z M1 Z1 M2 Z2,
  triangle_circumscription_principle ->
  A <> B ->
  A <> C ->
  A <> D ->
  A <> T ->
  A <> Y ->
  B <> C ->
  B <> D ->
  B <> T ->
  B <> Y ->
  C <> D ->
  C <> T ->
  C <> Y ->
  D <> T ->
  T <> X ->
  T <> Y ->
  X <> Y ->
  Y <> Z1 ->
  Y <> Z2 ->
  ~ Col A B C ->
  Col A B M1 ->
  Col A C M2 ->
  Bet A D T ->
  ~ Col B C T ->
  Bet B D C ->
  Col T Y Z ->
  Bet Y T X ->
  Bet Y M1 Z1 ->
  Bet Y M2 Z2 ->
  Cong Y T T X ->
  Cong Y M1 M1 Z1 ->
  Cong Y M2 M2 Z2 ->
  Perp B C T Z ->
  Perp A B Y Z1 ->
  Perp A C Y Z2 ->
  exists x, exists y, Bet A B x /\ Bet A C y /\ Bet x T y.
Proof.
(* Goal: forall (A B C D T X Y Z M1 Z1 M2 Z2 : @Tpoint Tn) (_ : @triangle_circumscription_principle 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) A Y)) (_ : not (@eq (@Tpoint Tn) B C)) (_ : not (@eq (@Tpoint Tn) B D)) (_ : not (@eq (@Tpoint Tn) B T)) (_ : not (@eq (@Tpoint Tn) B Y)) (_ : not (@eq (@Tpoint Tn) C D)) (_ : not (@eq (@Tpoint Tn) C T)) (_ : not (@eq (@Tpoint Tn) C Y)) (_ : not (@eq (@Tpoint Tn) D T)) (_ : not (@eq (@Tpoint Tn) T X)) (_ : not (@eq (@Tpoint Tn) T Y)) (_ : not (@eq (@Tpoint Tn) X Y)) (_ : not (@eq (@Tpoint Tn) Y Z1)) (_ : not (@eq (@Tpoint Tn) Y Z2)) (_ : not (@Col Tn A B C)) (_ : @Col Tn A B M1) (_ : @Col Tn A C M2) (_ : @Bet Tn A D T) (_ : not (@Col Tn B C T)) (_ : @Bet Tn B D C) (_ : @Col Tn T Y Z) (_ : @Bet Tn Y T X) (_ : @Bet Tn Y M1 Z1) (_ : @Bet Tn Y M2 Z2) (_ : @Cong Tn Y T T X) (_ : @Cong Tn Y M1 M1 Z1) (_ : @Cong Tn Y M2 M2 Z2) (_ : @Perp Tn B C T Z) (_ : @Perp Tn A B Y Z1) (_ : @Perp Tn A C Y Z2), @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 X Y Z M1 Z1 M2 Z2; intro HTC.
(* Goal: forall (_ : 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) A Y)) (_ : not (@eq (@Tpoint Tn) B C)) (_ : not (@eq (@Tpoint Tn) B D)) (_ : not (@eq (@Tpoint Tn) B T)) (_ : not (@eq (@Tpoint Tn) B Y)) (_ : not (@eq (@Tpoint Tn) C D)) (_ : not (@eq (@Tpoint Tn) C T)) (_ : not (@eq (@Tpoint Tn) C Y)) (_ : not (@eq (@Tpoint Tn) D T)) (_ : not (@eq (@Tpoint Tn) T X)) (_ : not (@eq (@Tpoint Tn) T Y)) (_ : not (@eq (@Tpoint Tn) X Y)) (_ : not (@eq (@Tpoint Tn) Y Z1)) (_ : not (@eq (@Tpoint Tn) Y Z2)) (_ : not (@Col Tn A B C)) (_ : @Col Tn A B M1) (_ : @Col Tn A C M2) (_ : @Bet Tn A D T) (_ : not (@Col Tn B C T)) (_ : @Bet Tn B D C) (_ : @Col Tn T Y Z) (_ : @Bet Tn Y T X) (_ : @Bet Tn Y M1 Z1) (_ : @Bet Tn Y M2 Z2) (_ : @Cong Tn Y T T X) (_ : @Cong Tn Y M1 M1 Z1) (_ : @Cong Tn Y M2 M2 Z2) (_ : @Perp Tn B C T Z) (_ : @Perp Tn A B Y Z1) (_ : @Perp Tn A C Y Z2), @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 HAB HAC HAD HAT HAY HBC HBD HBT HBY HCD HCT HCY HDT HTX HTY HXY HYZ1 HYZ2.
(* Goal: forall (_ : not (@Col Tn A B C)) (_ : @Col Tn A B M1) (_ : @Col Tn A C M2) (_ : @Bet Tn A D T) (_ : not (@Col Tn B C T)) (_ : @Bet Tn B D C) (_ : @Col Tn T Y Z) (_ : @Bet Tn Y T X) (_ : @Bet Tn Y M1 Z1) (_ : @Bet Tn Y M2 Z2) (_ : @Cong Tn Y T T X) (_ : @Cong Tn Y M1 M1 Z1) (_ : @Cong Tn Y M2 M2 Z2) (_ : @Perp Tn B C T Z) (_ : @Perp Tn A B Y Z1) (_ : @Perp Tn A C Y Z2), @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 HABC HABM1 HACM2 HADT HBCT HBDC HTYZ HYTX HYM1Z1.
(* Goal: forall (_ : @Bet Tn Y M2 Z2) (_ : @Cong Tn Y T T X) (_ : @Cong Tn Y M1 M1 Z1) (_ : @Cong Tn Y M2 M2 Z2) (_ : @Perp Tn B C T Z) (_ : @Perp Tn A B Y Z1) (_ : @Perp Tn A C Y Z2), @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 HYM2Z2 HCong5 HCong6 HCong7 HPerp1 HPerp2 HPerp3.
(* 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)))) *)
elim (col_dec X Y Z1); intro HXYZ1; elim (col_dec X Y Z2); intro HXYZ2.

(* 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)))) *)
(* 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)))) *)
(* 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)))) *)
(* 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)))) *)
  exfalso; apply HABC; apply par_id.
(* Goal: @Par Tn A B A C *)
(* 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)))) *)
(* 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)))) *)
(* 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)))) *)
  apply l12_9 with Y Z1; Perp.
(* Goal: @Coplanar Tn Y Z1 A A *)
(* Goal: @Coplanar Tn Y Z1 A C *)
(* Goal: @Coplanar Tn Y Z1 B A *)
(* Goal: @Coplanar Tn Y Z1 B C *)
(* Goal: @Perp Tn A C Y Z1 *)
(* 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)))) *)
(* 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)))) *)
(* 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 A; right; left; split; Col.
(* Goal: @Coplanar Tn Y Z1 A C *)
(* Goal: @Coplanar Tn Y Z1 B A *)
(* Goal: @Coplanar Tn Y Z1 B C *)
(* Goal: @Perp Tn A C Y Z1 *)
(* 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)))) *)
(* 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)))) *)
(* 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)))) *)
    apply coplanar_perm_16, col_cop__cop with Z2; Cop; ColR.
(* Goal: @Coplanar Tn Y Z1 B A *)
(* Goal: @Coplanar Tn Y Z1 B C *)
(* Goal: @Perp Tn A C Y Z1 *)
(* 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)))) *)
(* 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)))) *)
(* 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)))) *)
    Cop.
(* Goal: @Coplanar Tn Y Z1 B C *)
(* Goal: @Perp Tn A C Y Z1 *)
(* 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)))) *)
(* 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)))) *)
(* 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)))) *)
    assert_diffs; apply coplanar_perm_16, col2_cop__cop with T Z; Cop; ColR.
(* Goal: @Perp Tn A C Y Z1 *)
(* 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)))) *)
(* 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)))) *)
(* 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)))) *)
  apply perp_col1 with Z2; assert_diffs; Perp; ColR.

(* 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)))) *)
(* 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)))) *)
(* 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)))) *)
  exfalso; apply HABC; apply par_id_1.
(* Goal: @Par Tn B A B C *)
(* 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)))) *)
(* 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)))) *)
  assert (Coplanar B C Y Z1) by (assert_diffs; apply col2_cop__cop with T Z; Cop; ColR).
(* Goal: @Coplanar Tn Y Z1 B A *)
(* Goal: @Coplanar Tn Y Z1 B C *)
(* Goal: @Perp Tn A C Y Z1 *)
(* 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)))) *)
(* 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)))) *)
(* 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)))) *)
  apply l12_9 with Y Z1; [Cop..| |Perp|].
(* Goal: @Coplanar Tn Y Z2 A B *)
(* Goal: @Perp Tn C B Y Z2 *)
(* 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)))) *)
    apply coplanar_pseudo_trans with B C T; [assumption|..|Cop].
(* Goal: @Coplanar Tn Y Z1 B A *)
(* Goal: @Coplanar Tn Y Z1 B C *)
(* Goal: @Perp Tn A C Y Z1 *)
(* 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)))) *)
(* 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)))) *)
(* 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)))) *)
    assert_diffs; apply col_cop__cop with Z; Col; Cop.
(* Goal: @Coplanar Tn B C T Z2 *)
(* Goal: @Coplanar Tn B C T A *)
(* Goal: @Perp Tn C B Y Z2 *)
(* 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)))) *)
    assert_diffs; apply col_cop__cop with Z; Cop; ColR.
(* Goal: @Coplanar Tn B C T A *)
(* Goal: @Perp Tn C B Y Z2 *)
(* 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 D; left; split; Col.
(* Goal: @Perp Tn B C X Y *)
(* Goal: @Perp Tn x y X Y *)
  apply perp_sym; apply perp_col2 with T Z; Perp; assert_cols; ColR.

(* 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)))) *)
(* 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)))) *)
  exfalso; apply HABC; apply par_id_2.
(* Goal: @Par Tn C A C B *)
(* 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)))) *)
  assert (Coplanar B C Y Z2) by (assert_diffs; apply col2_cop__cop with T Z; Cop; ColR).
(* Goal: @Coplanar Tn Y Z1 B A *)
(* Goal: @Coplanar Tn Y Z1 B C *)
(* Goal: @Perp Tn A C Y Z1 *)
(* 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)))) *)
(* 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)))) *)
(* 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)))) *)
  apply l12_9 with Y Z2; [Cop..| |Perp|].
(* Goal: @Coplanar Tn Y Z2 A B *)
(* Goal: @Perp Tn C B Y Z2 *)
(* 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)))) *)
    apply coplanar_pseudo_trans with B C T; [assumption|..|Cop].
(* Goal: @Coplanar Tn Y Z1 B A *)
(* Goal: @Coplanar Tn Y Z1 B C *)
(* Goal: @Perp Tn A C Y Z1 *)
(* 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)))) *)
(* 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)))) *)
(* 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)))) *)
    assert_diffs; apply col_cop__cop with Z; Col; Cop.
(* Goal: @Coplanar Tn B C T Z2 *)
(* Goal: @Coplanar Tn B C T A *)
(* Goal: @Perp Tn C B Y Z2 *)
(* 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)))) *)
    assert_diffs; apply col_cop__cop with Z; Cop; ColR.
(* Goal: @Coplanar Tn B C T A *)
(* Goal: @Perp Tn C B Y Z2 *)
(* 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 D; left; split; Col.
(* Goal: @Perp Tn B C X Y *)
(* Goal: @Perp Tn x y X Y *)
  apply perp_sym; apply perp_col2 with T Z; Perp; assert_cols; ColR.

  assert (H := HXYZ1); apply HTC in H;
  destruct H as [x [HCong1 [HCong2 HCop1]]]; exists x;
  assert (H := HXYZ2); apply HTC in H;
  destruct H as [y [HCong3 [HCong4 HCop2]]]; exists y.
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
  assert (HYM1 : Y <> M1) by (intro; treat_equalities; auto).
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
  assert (HYM2 : Y <> M2) by (intro; treat_equalities; auto).
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
  assert (HCopA : Coplanar B C T A) by (exists D; left; split; Col).
(* Goal: @Coplanar Tn Y Z1 B A *)
(* Goal: @Coplanar Tn Y Z1 B C *)
(* Goal: @Perp Tn A C Y Z1 *)
(* 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)))) *)
(* 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)))) *)
(* 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)))) *)
  assert (HCopB : Coplanar B C T B) by Cop.
(* Goal: @Coplanar Tn Y Z1 B A *)
(* Goal: @Coplanar Tn Y Z1 B C *)
(* Goal: @Perp Tn A C Y Z1 *)
(* 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)))) *)
(* 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)))) *)
(* 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)))) *)
  assert (HCopC : Coplanar B C T C) by Cop.
(* Goal: @Coplanar Tn Y Z1 B A *)
(* Goal: @Coplanar Tn Y Z1 B C *)
(* Goal: @Perp Tn A C Y Z1 *)
(* 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)))) *)
(* 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)))) *)
(* 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)))) *)
  assert (HCopT : Coplanar B C T T) by Cop.
(* Goal: @Coplanar Tn Y Z1 B A *)
(* Goal: @Coplanar Tn Y Z1 B C *)
(* Goal: @Perp Tn A C Y Z1 *)
(* 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)))) *)
(* 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)))) *)
(* 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)))) *)
  assert (HCopZ : Coplanar B C T Z) by Cop.
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
  assert (HCopY : Coplanar B C T Y) by (assert_diffs; apply col_cop__cop with Z; Col).
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
  assert (HCopX : Coplanar B C T X) by (apply col_cop__cop with Y; Col).
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
  assert (HCopZ1 : Coplanar B C T Z1).
(* Goal: @Par Tn B C x y *)
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
  { assert (~ Col A B Y).
(* Goal: not (@Col Tn A B Y) *)
(* Goal: @Coplanar Tn B C T Z1 *)
      intro; destruct (perp_not_col2 A B Y Z1) as [|HNCol]; Perp; apply HNCol; ColR.
(* Goal: @Coplanar Tn Y Z1 B A *)
(* Goal: @Coplanar Tn Y Z1 B C *)
(* Goal: @Perp Tn A C Y Z1 *)
(* 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)))) *)
(* 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)))) *)
(* 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)))) *)
    apply coplanar_pseudo_trans with A B Y; [| |apply coplanar_pseudo_trans with B C T..|]; Cop.
  }
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
  assert (HCopZ2 : Coplanar B C T Z2).
(* Goal: @Par Tn B C x y *)
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
  { assert (~ Col A C Y).
(* Goal: not (@Col Tn A C Y) *)
(* Goal: @Coplanar Tn B C T Z2 *)
      intro; destruct (perp_not_col2 A C Y Z2) as [|HNCol]; Perp; apply HNCol; ColR.
    apply coplanar_pseudo_trans with A C Y;
(* Goal: @Coplanar Tn Y Z1 B A *)
(* Goal: @Coplanar Tn Y Z1 B C *)
(* Goal: @Perp Tn A C Y Z1 *)
(* 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)))) *)
(* 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)))) *)
(* 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)))) *)
    [|apply coplanar_pseudo_trans with B C T| |apply coplanar_pseudo_trans with B C T|]; Cop.
  }
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
  assert (HCopx : Coplanar B C T x).
(* Goal: @Coplanar Tn B C T x *)
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
    apply coplanar_pseudo_trans with X Y Z1; trivial; apply coplanar_pseudo_trans with B C T; assumption.
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
  assert (HCopy : Coplanar B C T y).
(* Goal: @Coplanar Tn B C T y *)
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
    apply coplanar_pseudo_trans with X Y Z2; trivial; apply coplanar_pseudo_trans with B C T; assumption.
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
  assert (HCop : Coplanar X Y x y).
(* Goal: @Coplanar Tn A y Y Z2 *)
(* Goal: @Cong Tn y Y y Z2 *)
(* Goal: @Perp_bisect Tn M2 A Y Z2 *)
    apply coplanar_pseudo_trans with B C T; assumption.
  assert (HxTy : Col x T y) by (elim (eq_dec_points T x); intro; elim (eq_dec_points T y);
                                intro; try (subst; Col); apply col_permutation_4;
                                apply cop_perp2__col with X Y; trivial; apply perp_bisect_perp;
                                apply cong_cop_perp_bisect; Cong; Cop).
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
  assert (HABx : Col A B x).
(* Goal: @Par Tn B C x y *)
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
    {
(* Goal: @Col Tn A B x *)
    elim (eq_dec_points A M1); intro HAM1; subst.

(* Goal: @Par Tn B C x y *)
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
      {
(* Goal: @Col Tn M1 A x *)
      apply cong_cop2_perp_bisect_col with Y Z1; trivial.
(* Goal: @Coplanar Tn M1 x Y Z1 *)
(* Goal: @Coplanar Tn A x Y Z1 *)
(* Goal: @Cong Tn x Y x Z1 *)
(* Goal: @Perp_bisect Tn M1 A Y Z1 *)
        exists M1; left; split; Col.
(* Goal: @Coplanar Tn A y Y Z2 *)
(* Goal: @Cong Tn y Y y Z2 *)
(* Goal: @Perp_bisect Tn M2 A Y Z2 *)
        apply coplanar_pseudo_trans with B C T; assumption.
(* Goal: @Cong Tn x Y x Z1 *)
(* Goal: @Perp_bisect Tn M1 A Y Z1 *)
        apply cong_transitivity with X x; Cong.
(* Goal: @Perp_bisect Tn M2 A Y Z2 *)
      apply perp_mid_perp_bisect; try split; Cong.
      }

(* Goal: @Par Tn B C x y *)
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
      {
(* Goal: @Col Tn A B x *)
      assert (Col M1 A x).
(* Goal: @Par Tn B C x y *)
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
        {
(* Goal: @Col Tn M1 A x *)
        apply cong_cop2_perp_bisect_col with Y Z1; trivial.
(* Goal: @Coplanar Tn M1 x Y Z1 *)
(* Goal: @Coplanar Tn A x Y Z1 *)
(* Goal: @Cong Tn x Y x Z1 *)
(* Goal: @Perp_bisect Tn M1 A Y Z1 *)
          exists M1; left; split; Col.
(* Goal: @Coplanar Tn A y Y Z2 *)
(* Goal: @Cong Tn y Y y Z2 *)
(* Goal: @Perp_bisect Tn M2 A Y Z2 *)
          apply coplanar_pseudo_trans with B C T; assumption.
(* Goal: @Cong Tn x Y x Z1 *)
(* Goal: @Perp_bisect Tn M1 A Y Z1 *)
          apply cong_transitivity with X x; Cong.
(* Goal: @Perp_bisect Tn M2 A Y Z2 *)
        apply perp_mid_perp_bisect; try split; Cong.
(* Goal: @Perp Tn M1 A Y Z1 *)
        apply perp_left_comm; apply perp_col with B; Col.
        }
(* Goal: @Col Tn A C y *)
      ColR.
      }
    }

(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
  assert (HACy : Col A C y).
(* Goal: @Par Tn B C x y *)
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
    {
(* Goal: @Col Tn A C y *)
    elim (eq_dec_points A M2); intro HAM1; subst.

(* Goal: @Par Tn B C x y *)
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
      {
(* Goal: @Col Tn M2 A y *)
      apply cong_cop2_perp_bisect_col with Y Z2; trivial.
(* Goal: @Coplanar Tn M2 y Y Z2 *)
(* Goal: @Coplanar Tn A y Y Z2 *)
(* Goal: @Cong Tn y Y y Z2 *)
(* Goal: @Perp_bisect Tn M2 A Y Z2 *)
        exists M2; left; split; Col.
(* Goal: @Coplanar Tn A y Y Z2 *)
(* Goal: @Cong Tn y Y y Z2 *)
(* Goal: @Perp_bisect Tn M2 A Y Z2 *)
        apply coplanar_pseudo_trans with B C T; assumption.
(* Goal: @Cong Tn y Y y Z2 *)
(* Goal: @Perp_bisect Tn M2 A Y Z2 *)
        apply cong_transitivity with X y; Cong.
(* Goal: @Perp_bisect Tn M2 A Y Z2 *)
      apply perp_mid_perp_bisect; try split; Cong.
      }

(* Goal: @Par Tn B C x y *)
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
      {
(* Goal: @Col Tn A C y *)
      assert (Col M2 A y).
(* Goal: @Par Tn B C x y *)
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
        {
(* Goal: @Col Tn M2 A y *)
        apply cong_cop2_perp_bisect_col with Y Z2; trivial.
(* Goal: @Coplanar Tn M2 y Y Z2 *)
(* Goal: @Coplanar Tn A y Y Z2 *)
(* Goal: @Cong Tn y Y y Z2 *)
(* Goal: @Perp_bisect Tn M2 A Y Z2 *)
          exists M2; left; split; Col.
(* Goal: @Coplanar Tn A y Y Z2 *)
(* Goal: @Cong Tn y Y y Z2 *)
(* Goal: @Perp_bisect Tn M2 A Y Z2 *)
          apply coplanar_pseudo_trans with B C T; assumption.
(* Goal: @Cong Tn y Y y Z2 *)
(* Goal: @Perp_bisect Tn M2 A Y Z2 *)
          apply cong_transitivity with X y; Cong.
(* Goal: @Perp_bisect Tn M2 A Y Z2 *)
        apply perp_mid_perp_bisect; try split; Cong.
(* Goal: @Perp Tn M2 A Y Z2 *)
        apply perp_left_comm; apply perp_col with C; Col.
        }
(* Goal: @Col Tn A C y *)
      ColR.
      }
    }
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
  assert (Hxy : x <> y).
(* Goal: @Par Tn B C x y *)
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
  {
(* Goal: not (@eq (@Tpoint Tn) x y) *)
    intro; treat_equalities.
(* Goal: False *)
    assert (A = x) by (apply l6_21 with A B C A; Col); treat_equalities.
(* Goal: False *)
    assert (H : Par B C A T).
(* Goal: @Par Tn B C x y *)
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
    {
(* Goal: @Par Tn B C x y *)
      apply l12_9 with X Y; try (apply coplanar_pseudo_trans with B C T; assumption).

(* Goal: @Col Tn A C y *)
        apply perp_sym; apply perp_col2 with Z T; Perp; assert_cols; ColR.
(* Goal: @Perp Tn A T X Y *)
        apply perp_bisect_perp; apply cong_cop_perp_bisect; Cong.
(* Goal: @Coplanar Tn A T X Y *)
        exists T; left; split; Col.
    }
(* Goal: False *)
    elim H; clear H; intro H.

(* Goal: False *)
(* Goal: False *)
      apply H; exists D; assert_cols; Col.

(* Goal: @Col Tn A C y *)
      spliter; apply HABC; assert_cols; ColR.
  }
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
  assert (HPar : Par B C x y).
(* Goal: @Par Tn B C x y *)
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
  {
(* Goal: @Par Tn B C x y *)
    apply l12_9 with X Y; try (apply coplanar_pseudo_trans with B C T; assumption).

(* Goal: @Perp Tn B C X Y *)
(* Goal: @Perp Tn x y X Y *)
      apply perp_sym; apply perp_col2 with T Z; Perp; assert_cols; ColR.

(* Goal: @Coplanar Tn Y Z1 B A *)
(* Goal: @Coplanar Tn Y Z1 B C *)
(* Goal: @Perp Tn A C Y Z1 *)
(* 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)))) *)
(* 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)))) *)
(* 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)))) *)
      apply perp_bisect_perp; apply cong_cop_perp_bisect; Cong; Cop.
  }
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
  clear HPerp1; clear HPerp2; clear HPerp3.
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
  clear HCong1; clear HCong2; clear HCong3; clear HCong4.
  assert (HPar' : Par_strict B C x y)
    by (elim HPar; clear HPar; intro HPar; try assumption; spliter; exfalso; apply HABC; assert_cols; ColR);
  clear HPar; rename HPar' into HPar.
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
  elim HxTy; clear HxTy; intro HxTy.

(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
    elim HABx; clear HABx; intro HABx.

(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
      elim HACy; clear HACy; intro HACy; auto.
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
      elim HACy; clear HACy; intro HACy.

(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
        exfalso; apply impossible_case_1 with A B C D T x y; assumption.

(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
        exfalso; apply impossible_case_2 with A B C D T x y; assert_cols; Col.

(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
      elim HABx; clear HABx; intro HABx.

(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
        exfalso; apply impossible_case_3 with A B C D T x y; assumption.

(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
        exfalso; apply impossible_case_2 with A C B D T y x; assert_cols; Col; Between.

(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
    elim HxTy; clear HxTy; intro HxTy.

(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
      exfalso; apply impossible_case_4 with A B C D T x y; assumption.

(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
      exfalso; apply impossible_case_4 with A C B D T y x; Between; Col; Par.
Qed.

Lemma triangle_circumscription_implies_tarski_s_euclid :
  triangle_circumscription_principle ->
  tarski_s_parallel_postulate.
Proof.
unfold tarski_s_parallel_postulate.
intro HTC; apply tarski_s_euclid_remove_degenerated_cases.
intros A B C D T HAB HAC HAD HAT HBC HBD HBT HCD HCT HDT HABC HADT HBDC;
assert (HBCT : ~ Col B C T) by (intro; apply HABC; assert_cols; ColR).
assert (HY := l8_18_existence B C T HBCT); destruct HY as [Y [HBCY HPerp]].
elim (eq_dec_points B Y); intro HBY; elim (eq_dec_points C Y); intro HCY; treat_equalities.

(* Goal: @Par Tn B C x y *)
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
  {
  exfalso; apply HBCT; Col.
  }

(* Goal: @Par Tn B C x y *)
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
  {
  assert (HY := midpoint_existence B T); destruct HY as [Y HY].
  assert (HAY : A <> Y) by (intro; treat_equalities; assert_cols; apply HABC; ColR).
  assert (H := midpoint_distinct_1 Y B T HBT HY); destruct H as [HBY HTY];
  apply not_eq_sym in HBY; apply not_eq_sym in HTY.
  assert (HCY : C <> Y) by (intro; subst; apply HBCT; assert_cols; Col).
  destruct HY as [HBTY HBYTY].
  assert (HACY : ~ Col A C Y) by (apply impossible_two_sides_not_col with B D T; assumption).
  assert (HX := symmetric_point_construction Y T); destruct HX as [X HX].
  assert (H := midpoint_distinct_2 T Y X HTY HX); destruct H as [HTX HXY]; apply not_eq_sym in HTX.
  destruct HX as [HXTY HXTYT].
  assert (HZ1 := l10_2_existence A B Y); destruct HZ1 as [Z1 HZ1].
  elim HZ1; clear HZ1; intro HZ1; destruct HZ1 as [Hclear HZ1]; try contradiction; clear Hclear.
  destruct HZ1 as [[M1 [[HXM1Z1 HM1XM1Z1] HABM1]] HZ1].
  assert (HZ2 := l10_2_existence A C Y); destruct HZ2 as [Z2 HZ2].
  elim HZ2; clear HZ2; intro HZ2; destruct HZ2 as [Hclear HZ2]; try contradiction; clear Hclear.
  destruct HZ2 as [[M2 [[HXM2Z2 HM2XM2Z2] HACM2]] HZ2].
  elim (eq_dec_points Y Z1); intro HYZ1; treat_equalities.

(* Goal: @Par Tn B C x y *)
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
    {
    assert (HFalse : Col A B C) by (assert_cols; ColR); contradiction.
    }

(* Goal: @Par Tn B C x y *)
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
    {
    elim HZ1; clear HZ1; intro HZ1; try contradiction.
    elim (eq_dec_points Y Z2); intro HYZ2; treat_equalities; try contradiction.
    elim HZ2; clear HZ2; intro HZ2; try contradiction.
    apply triangle_circumscription_implies_tarski_s_euclid_aux with D X Y B M1 Z1 M2 Z2; try assumption.
    assert_cols; Col.
    }
  }

(* Goal: @Par Tn B C x y *)
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
  {
  assert (HY := midpoint_existence C T); destruct HY as [Y HY].
  assert (HAY : A <> Y) by (intro; treat_equalities; assert_cols; apply HABC; ColR).
  assert (H := midpoint_distinct_1 Y C T HCT HY); destruct H as [HCY HTY];
  apply not_eq_sym in HCY; apply not_eq_sym in HTY.
  assert (HBY : B <> Y) by (intro; subst; apply HBCT; assert_cols; Col).
  destruct HY as [HCTY HCYTY].
  assert (HACY : ~ Col A B Y) by (apply impossible_two_sides_not_col with C D T; Between; Col).
  assert (HX := symmetric_point_construction Y T); destruct HX as [X HX].
  assert (H := midpoint_distinct_2 T Y X HTY HX); destruct H as [HTX HXY]; apply not_eq_sym in HTX.
  destruct HX as [HXTY HXTYT].
  assert (HZ1 := l10_2_existence A B Y); destruct HZ1 as [Z1 HZ1].
  elim HZ1; clear HZ1; intro HZ1; destruct HZ1 as [Hclear HZ1]; try contradiction; clear Hclear.
  destruct HZ1 as [[M1 [[HXM1Z1 HM1XM1Z1] HABM1]] HZ1].
  assert (HZ2 := l10_2_existence A C Y); destruct HZ2 as [Z2 HZ2].
  elim HZ2; clear HZ2; intro HZ2; destruct HZ2 as [Hclear HZ2]; try contradiction; clear Hclear.
  destruct HZ2 as [[M2 [[HXM2Z2 HM2XM2Z2] HACM2]] HZ2].
  elim (eq_dec_points Y Z2); intro HYZ2; treat_equalities.

(* Goal: @Par Tn B C x y *)
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
    {
    assert (HFalse : Col A B C) by (assert_cols; ColR); contradiction.
    }

(* Goal: @Par Tn B C x y *)
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
    {
    elim HZ2; clear HZ2; intro HZ2; try contradiction.
    elim (eq_dec_points Y Z1); intro HYZ1; treat_equalities; try contradiction.
    elim HZ1; clear HZ1; intro HZ1; try contradiction.
    apply triangle_circumscription_implies_tarski_s_euclid_aux with D X Y C M1 Z1 M2 Z2; try assumption.
    assert_cols; Col.
    }
  }

(* Goal: @Par Tn B C x y *)
(* Goal: and (@Bet Tn A B x) (and (@Bet Tn A C y) (@Bet Tn x T y)) *)
  {
  assert (HAY : A <> Y) by (intro; treat_equalities; assert_cols; apply HABC; ColR).
  assert (HX := symmetric_point_construction Y T); destruct HX as [X HX].
  assert (H := perp_distinct B C T Y HPerp); destruct H as [Hclear HTY]; clear Hclear.
  assert (H := midpoint_distinct_2 T Y X HTY HX); destruct H as [HTX HXY]; apply not_eq_sym in HTX.
  destruct HX as [HXTY HXTYT].
  assert (HZ1 := l10_2_existence A B Y); destruct HZ1 as [Z1 HZ1].
  elim HZ1; clear HZ1; intro HZ1; destruct HZ1 as [Hclear HZ1]; try contradiction; clear Hclear.
  destruct HZ1 as [[M1 [[HXM1Z1 HM1XM1Z1] HABM1]] HZ1].
  assert (HZ2 := l10_2_existence A C Y); destruct HZ2 as [Z2 HZ2].
  elim HZ2; clear HZ2; intro HZ2; destruct HZ2 as [Hclear HZ2]; try contradiction; clear Hclear.
  destruct HZ2 as [[M2 [[HXM2Z2 HM2XM2Z2] HACM2]] HZ2].
  assert (HABY : ~ Col A B Y) by (intro; apply HBY; apply l6_21 with A B C B; assert_cols; Col).
  assert (HACY : ~ Col A C Y) by (intro; apply HCY; apply l6_21 with A C B C; assert_cols; Col).
  elim (eq_dec_points Y Z1); intro HYZ1; treat_equalities; try contradiction.
  elim HZ1; clear HZ1; intro HZ1; try contradiction.
  elim (eq_dec_points Y Z2); intro HYZ2; treat_equalities; try contradiction.
  elim HZ2; clear HZ2; intro HZ2; try contradiction.
  apply triangle_circumscription_implies_tarski_s_euclid_aux with D X Y Y M1 Z1 M2 Z2; Col.
  }
Qed.

End TCP_tarski.