Require Import GeoCoq.Axioms.parallel_postulates.
Require Import GeoCoq.Tarski_dev.Ch12_parallel.

Section par_trans_NID.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma par_dec_NID : decidability_of_parallelism <-> decidability_of_not_intersection.
Proof.
(* Goal: iff (@decidability_of_parallelism Tn) (@decidability_of_not_intersection Tn) *)
split; intros Hdec A B C D; destruct (cop_dec A B C D) as [|HNCop].
- destruct (Hdec A B C D) as [[HParS|Heq]|HNPar].
  * left; unfold Par_strict in HParS; spliter; assumption.
  * right; intro Habs; apply Habs; exists B; spliter; Col.
  * right; intro Habs.
(* Goal: or (@Par Tn A B C D) (not (@Par Tn A B C D)) *)
    destruct (eq_dec_points A B).
(* Goal: False *)
(* Goal: False *)
      apply Habs; exists C; subst; split; Col.
(* Goal: or (@Par Tn A B C D) (not (@Par Tn A B C D)) *)
    destruct (eq_dec_points C D).
(* Goal: False *)
(* Goal: False *)
      apply Habs; exists A; subst; split; Col.
(* Goal: False *)
    apply HNPar; left; unfold Par_strict; repeat split; assumption.

- left; intros [I []]; apply HNCop; exists I; left; split; Col.

- destruct (eq_dec_points A B).
(* Goal: or (@Par Tn A B C D) (not (@Par Tn A B C D)) *)
(* Goal: or (@Par Tn A B C D) (not (@Par Tn A B C D)) *)
    right; subst; intro; assert_diffs; auto.
(* Goal: or (@Par Tn A B C D) (not (@Par Tn A B C D)) *)
  destruct (eq_dec_points C D).
(* Goal: or (@Par Tn A B C D) (not (@Par Tn A B C D)) *)
(* Goal: or (@Par Tn A B C D) (not (@Par Tn A B C D)) *)
    right; subst; intro; assert_diffs; auto.
(* Goal: or (@Par Tn A B C D) (not (@Par Tn A B C D)) *)
  destruct (col_dec A C D).

(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => not (and (not (and (@Col Tn A1 A2 I) (@Col Tn C1 C2 I))) (and (not (and (@Col Tn A1 C1 I) (@Col Tn A2 C2 I))) (not (and (@Col Tn A1 C2 I) (@Col Tn A2 C1 I)))))) *)
  {
(* Goal: or (@Par Tn A B C D) (not (@Par Tn A B C D)) *)
    destruct (col_dec B C D).
(* Goal: or (@Par Tn A B C D) (not (@Par Tn A B C D)) *)
(* Goal: or (@Par Tn A B C D) (not (@Par Tn A B C D)) *)
      left; right; repeat split; assumption.
(* Goal: or (@Par Tn A B C D) (not (@Par Tn A B C D)) *)
    right; intros [[_ [_ [_ Habs]]]|].
(* Goal: False *)
(* Goal: False *)
      apply Habs; exists A; split; Col.
(* Goal: False *)
    spliter; auto.
  }

(* Goal: or (@Par Tn A B C D) (not (@Par Tn A B C D)) *)
  destruct (Hdec A B C D) as [HPar|HNPar].
(* Goal: or (@Par Tn A B C D) (not (@Par Tn A B C D)) *)
(* Goal: or (@Par Tn A B C D) (not (@Par Tn A B C D)) *)
    left; left; repeat split; assumption.
(* Goal: or (@Par Tn A B C D) (not (@Par Tn A B C D)) *)
  right.
(* Goal: not (@Par Tn A B C D) *)
  intros [HParS|Heq].
(* Goal: False *)
(* Goal: False *)
    apply HNPar; unfold Par_strict in HParS; spliter; assumption.
(* Goal: False *)
  spliter; auto.

- right; intro HPar; apply HNCop, par__coplanar, HPar.
Qed.

Lemma par_trans__par_dec :
  postulate_of_transitivity_of_parallelism ->
  decidability_of_parallelism.
Proof.
(* Goal: forall _ : @postulate_of_transitivity_of_parallelism Tn, @decidability_of_parallelism Tn *)
intros HTP A B C D.
elim (eq_dec_points A B); intro HAB;
[treat_equalities; right; intro; assert_diffs; intuition|].
elim (eq_dec_points C D); intro HCD;
[treat_equalities; right; intro; assert_diffs; intuition|].
(* Goal: or (@Par Tn A B C D) (not (@Par Tn A B C D)) *)
destruct (parallel_existence1 A B C HAB) as [D' HPar].
elim (col_dec C D D'); intro HCol;
[left; apply par_col_par with D'; Par; Col|
 right; intro; apply HCol; apply par_id_3; apply HTP with A B; Par].
Qed.

Lemma col_int : forall A B C,
  Col A B C <-> ~ (~ Bet A B C /\ ~ Bet B C A /\ ~ Bet C A B).
Proof.
(* Goal: forall A B C : @Tpoint Tn, iff (@Col Tn A B C) (not (and (not (@Bet Tn A B C)) (and (not (@Bet Tn B C A)) (not (@Bet Tn C A B))))) *)
intros A B C; unfold Col.
induction (bet_dec A B C); induction (bet_dec B C A); induction (bet_dec C A B);
intuition.
Qed.

Definition playfair_ter := forall A1 A2 B1 B2 C1 C2 P,
  A1 <> A2 -> B1 <> B2 -> C1 <> C2 ->
  Col P B1 B2 -> Col P C1 C2 ->
  ~ (Col A1 B1 B2 /\ Col A2 B1 B2) ->
  ~ (Col A1 C1 C2 /\ Col A2 C1 C2) ->
  ~ (Col C1 B1 B2 /\ Col C2 B1 B2) ->
  (exists I, ~ (~ (Col A1 A2 I /\ Col B1 B2 I) /\
                ~ (Col A1 B1 I /\ Col A2 B2 I) /\
                ~ (Col A1 B2 I /\ Col A2 B1 I))) ->
  (exists I, ~ (~ (Col A1 A2 I /\ Col C1 C2 I) /\
               ~ (Col A1 C1 I /\ Col A2 C2 I) /\
               ~ (Col A1 C2 I /\ Col A2 C1 I))) ->
  ~ (~ (exists I, Col I A1 A2 /\ Col I B1 B2) /\
     ~ (exists I, Col I A1 A2 /\ Col I C1 C2)).

Definition playfair_quater_qf A1 A2 B1 B2 C1 C2 P :=
  A1 <> A2 /\ B1 <> B2 /\ C1 <> C2 /\
  Col P B1 B2 /\ Col P C1 C2 /\
  ~ (Col A1 B1 B2 /\ Col A2 B1 B2) /\
  ~ (Col A1 C1 C2 /\ Col A2 C1 C2) /\
  ~ (Col C1 B1 B2 /\ Col C2 B1 B2) /\
  (exists I, ~ (~ (Col A1 A2 I /\ Col B1 B2 I) /\
                ~ (Col A1 B1 I /\ Col A2 B2 I) /\
                ~ (Col A1 B2 I /\ Col A2 B1 I))) /\
  (exists I, ~ (~ (Col A1 A2 I /\ Col C1 C2 I) /\
                ~ (Col A1 C1 I /\ Col A2 C2 I) /\
                ~ (Col A1 C2 I /\ Col A2 C1 I))) /\
  ~ (exists I, Col I A1 A2 /\ Col I B1 B2) /\
  ~ (exists I, Col I A1 A2 /\ Col I C1 C2).

Definition playfair_quater := ~ exists A1 A2 B1 B2 C1 C2 P,
  playfair_quater_qf A1 A2 B1 B2 C1 C2 P.

Lemma playfair__playfair_ter :
  playfair_s_postulate -> playfair_ter.
Proof.
(* Goal: forall _ : @playfair_s_postulate Tn, playfair_ter *)
intros HP A1 A2 B1 B2 C1 C2 P HA HB HC HP1 HP2 HNC1 HNC2 HNC3 HIAB HIAC.
(* Goal: not (and (not (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I A1 A2) (@Col Tn I B1 B2)))) (not (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I A1 A2) (@Col Tn I C1 C2))))) *)
intros [HAB HAC]. apply HNC3.
apply (HP A1 A2 B1 B2 C1 C2 P); Col; left;
repeat (split; Col).

(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => not (and (not (and (@Col Tn A1 A2 I) (@Col Tn C1 C2 I))) (and (not (and (@Col Tn A1 C1 I) (@Col Tn A2 C2 I))) (not (and (@Col Tn A1 C2 I) (@Col Tn A2 C1 I)))))) *)
  {
(* Goal: @Coplanar Tn A1 A2 B1 B2 *)
  destruct HIAB as [IAB HIAB]; exists IAB.
(* Goal: or (and (@Col Tn A1 A2 IAB) (@Col Tn B1 B2 IAB)) (or (and (@Col Tn A1 B1 IAB) (@Col Tn A2 B2 IAB)) (and (@Col Tn A1 B2 IAB) (@Col Tn A2 B1 IAB))) *)
  clear HA HB HC HP1 HP2 HNC1 HNC2 HNC3 HIAC HAB HAC P C1 C2.
  induction (col_dec A1 A2 IAB); induction (col_dec B1 B2 IAB);
  try solve [left; Col];
  induction (col_dec A1 B1 IAB); induction (col_dec A2 B2 IAB);
  try solve [right; left; Col];
  induction (col_dec A1 B2 IAB); induction (col_dec A2 B1 IAB);
  try solve [right; right; Col];
  exfalso; apply HIAB; intuition.
  }

(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => not (and (not (and (@Col Tn A1 A2 I) (@Col Tn C1 C2 I))) (and (not (and (@Col Tn A1 C1 I) (@Col Tn A2 C2 I))) (not (and (@Col Tn A1 C2 I) (@Col Tn A2 C1 I)))))) *)
  {
(* Goal: @Coplanar Tn A1 A2 C1 C2 *)
  destruct HIAC as [IAC HIAC]; exists IAC.
(* Goal: or (and (@Col Tn A1 A2 IAC) (@Col Tn C1 C2 IAC)) (or (and (@Col Tn A1 C1 IAC) (@Col Tn A2 C2 IAC)) (and (@Col Tn A1 C2 IAC) (@Col Tn A2 C1 IAC))) *)
  clear HA HB HC HP1 HP2 HNC1 HNC2 HNC3 HIAB HAB HAC P B1 B2.
  induction (col_dec A1 A2 IAC); induction (col_dec C1 C2 IAC);
  try solve [left; Col];
  induction (col_dec A1 C1 IAC); induction (col_dec A2 C2 IAC);
  try solve [right; left; Col];
  induction (col_dec A1 C2 IAC); induction (col_dec A2 C1 IAC);
  try solve [right; right; Col];
  exfalso; apply HIAC; intuition.
  }
Qed.

Lemma playfair__playfair_quater :
  playfair_s_postulate -> playfair_quater.
Proof.
(* Goal: forall _ : @playfair_s_postulate Tn, playfair_quater *)
intro HP; intro HPQ; destruct HPQ as [A1 [A2 [B1 [B2 [C1 [C2 [P HPQ]]]]]]].
(* Goal: False *)
assert (H:= HP A1 A2 B1 B2 C1 C2 P); clear HP.
(* Goal: False *)
destruct HPQ as [HD1 [HD2 [HD3 [HC1 [HC2 [HNC1 [HNC2 [HNC3 HPQ]]]]]]]].
(* Goal: False *)
destruct HPQ as [HIAB [HIAC [HNI1 HNI2]]].
apply HNC3; apply H; clear H; Col; left;
repeat (split; try assumption); auto.


(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => not (and (not (and (@Col Tn A1 A2 I) (@Col Tn C1 C2 I))) (and (not (and (@Col Tn A1 C1 I) (@Col Tn A2 C2 I))) (not (and (@Col Tn A1 C2 I) (@Col Tn A2 C1 I)))))) *)
  {
(* Goal: @Coplanar Tn A1 A2 B1 B2 *)
  destruct HIAB as [IAB HIAB]; exists IAB.
(* Goal: or (and (@Col Tn A1 A2 IAB) (@Col Tn B1 B2 IAB)) (or (and (@Col Tn A1 B1 IAB) (@Col Tn A2 B2 IAB)) (and (@Col Tn A1 B2 IAB) (@Col Tn A2 B1 IAB))) *)
  clear HD1 HD2 HD3 HC1 HC2 HNC1 HNC2 HNC3 HIAC HNI1 HNI2 P C1 C2.
  induction (col_dec A1 A2 IAB); induction (col_dec B1 B2 IAB);
  try solve [left; Col];
  induction (col_dec A1 B1 IAB); induction (col_dec A2 B2 IAB);
  try solve [right; left; Col];
  induction (col_dec A1 B2 IAB); induction (col_dec A2 B1 IAB);
  try solve [right; right; Col];
  exfalso; apply HIAB; intuition.
  }

(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => not (and (not (and (@Col Tn A1 A2 I) (@Col Tn C1 C2 I))) (and (not (and (@Col Tn A1 C1 I) (@Col Tn A2 C2 I))) (not (and (@Col Tn A1 C2 I) (@Col Tn A2 C1 I)))))) *)
  {
(* Goal: @Coplanar Tn A1 A2 C1 C2 *)
  destruct HIAC as [IAC HIAC]; exists IAC.
(* Goal: or (and (@Col Tn A1 A2 IAC) (@Col Tn C1 C2 IAC)) (or (and (@Col Tn A1 C1 IAC) (@Col Tn A2 C2 IAC)) (and (@Col Tn A1 C2 IAC) (@Col Tn A2 C1 IAC))) *)
  clear HD1 HD2 HD3 HC1 HC2 HNC1 HNC2 HNC3 HIAB HNI1 HNI2 P B1 B2.
  induction (col_dec A1 A2 IAC); induction (col_dec C1 C2 IAC);
  try solve [left; Col];
  induction (col_dec A1 C1 IAC); induction (col_dec A2 C2 IAC);
  try solve [right; left; Col];
  induction (col_dec A1 C2 IAC); induction (col_dec A2 C1 IAC);
  try solve [right; right; Col];
  exfalso; apply HIAC; intuition.
  }
Qed.

Lemma playfair_ter__playfair :
  playfair_ter -> playfair_s_postulate.
Proof.
(* Goal: forall _ : playfair_quater, @playfair_s_postulate Tn *)
intros HP A1 A2 B1 B2 C1 C2 P HPar1 HP1 HPar2 HP2.
elim (col_dec A1 B1 B2); intro HNC1.

(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => not (and (not (and (@Col Tn A1 A2 I) (@Col Tn C1 C2 I))) (and (not (and (@Col Tn A1 C1 I) (@Col Tn A2 C2 I))) (not (and (@Col Tn A1 C2 I) (@Col Tn A2 C1 I)))))) *)
  {
(* Goal: False *)
  assert (HA : A1 <> A2) by (assert_diffs; auto).
(* Goal: False *)
  assert (HB : B1 <> B2) by (assert_diffs; auto).
(* Goal: False *)
  assert (HC : C1 <> C2) by (assert_diffs; auto).
  apply (not_strict_par _ _ _ _ A1) in HPar1; Col.
  destruct HPar1 as [HC1 HC2]; clear HNC1.
  apply (not_strict_par _ _ _ _ P) in HPar2; spliter; try split; ColR.
  }

(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => not (and (not (and (@Col Tn A1 A2 I) (@Col Tn C1 C2 I))) (and (not (and (@Col Tn A1 C1 I) (@Col Tn A2 C2 I))) (not (and (@Col Tn A1 C2 I) (@Col Tn A2 C1 I)))))) *)
  {
  elim (col_dec A1 C1 C2); intro HNC2.

(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => not (and (not (and (@Col Tn A1 A2 I) (@Col Tn C1 C2 I))) (and (not (and (@Col Tn A1 C1 I) (@Col Tn A2 C2 I))) (not (and (@Col Tn A1 C2 I) (@Col Tn A2 C1 I)))))) *)
    {
(* Goal: False *)
    assert (HA : A1 <> A2) by (assert_diffs; auto).
(* Goal: False *)
    assert (HB : B1 <> B2) by (assert_diffs; auto).
(* Goal: False *)
    assert (HC : C1 <> C2) by (assert_diffs; auto).
    apply (not_strict_par _ _ _ _ A1) in HPar2; Col.
    destruct HPar2 as [HC1 HC2]; clear HNC2.
    apply (not_strict_par _ _ _ _ P) in HPar1; spliter; try split; ColR.
    }

(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => not (and (not (and (@Col Tn A1 A2 I) (@Col Tn C1 C2 I))) (and (not (and (@Col Tn A1 C1 I) (@Col Tn A2 C2 I))) (not (and (@Col Tn A1 C2 I) (@Col Tn A2 C1 I)))))) *)
    {
    assert (H : ~ ~ (Col C1 B1 B2 /\ Col C2 B1 B2) ->
                Col C1 B1 B2 /\ Col C2 B1 B2);
    [induction (col_dec C1 B1 B2); induction (col_dec C2 B1 B2); intuition|
     apply H; clear H; intro HNC3; apply (HP A1 A2 B1 B2 C1 C2 P);
     try solve [assert_diffs; Col]; try (intros [HC1 HC2]; intuition)].

(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => not (and (not (and (@Col Tn A1 A2 I) (@Col Tn C1 C2 I))) (and (not (and (@Col Tn A1 C1 I) (@Col Tn A2 C2 I))) (not (and (@Col Tn A1 C2 I) (@Col Tn A2 C1 I)))))) *)
      {
      apply par_symmetry in HPar1.
      apply (par_not_col_strict _ _ _ _ A1) in HPar1; Col.
      destruct HPar1 as [_ [_ [[IAB HIAB] _]]].
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => not (and (not (and (@Col Tn A1 A2 I) (@Col Tn B1 B2 I))) (and (not (and (@Col Tn A1 B1 I) (@Col Tn A2 B2 I))) (not (and (@Col Tn A1 B2 I) (@Col Tn A2 B1 I)))))) *)
      exists IAB; intros [HIAB1 [HIAB2 HIAB3]].
      elim HIAB; clear HIAB; intro HIAB; [apply HIAB1|];
      try solve [spliter; split; Col].
      elim HIAB; clear HIAB; intro HIAB; [apply HIAB2|apply HIAB3];
      spliter; split; Col.
      }

(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => not (and (not (and (@Col Tn A1 A2 I) (@Col Tn C1 C2 I))) (and (not (and (@Col Tn A1 C1 I) (@Col Tn A2 C2 I))) (not (and (@Col Tn A1 C2 I) (@Col Tn A2 C1 I)))))) *)
      {
      apply par_symmetry in HPar2.
      apply (par_not_col_strict _ _ _ _ A1) in HPar2; Col.
      destruct HPar2 as [_ [_ [[IAC HIAC] _]]].
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => not (and (not (and (@Col Tn A1 A2 I) (@Col Tn C1 C2 I))) (and (not (and (@Col Tn A1 C1 I) (@Col Tn A2 C2 I))) (not (and (@Col Tn A1 C2 I) (@Col Tn A2 C1 I)))))) *)
      exists IAC; intros [HIAC1 [HIAC2 HIAC3]].
      elim HIAC; clear HIAC; intro HIAC; [apply HIAC1|];
      try solve [spliter; split; Col].
      elim HIAC; clear HIAC; intro HIAC; [apply HIAC2|apply HIAC3];
      spliter; split; Col.
      }

(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => not (and (not (and (@Col Tn A1 A2 I) (@Col Tn C1 C2 I))) (and (not (and (@Col Tn A1 C1 I) (@Col Tn A2 C2 I))) (not (and (@Col Tn A1 C2 I) (@Col Tn A2 C1 I)))))) *)
      {
      apply par_symmetry in HPar1; apply par_symmetry in HPar2.
      apply (par_not_col_strict _ _ _ _ A1) in HPar1; Col.
      apply (par_not_col_strict _ _ _ _ A1) in HPar2; Col.
      destruct HPar1 as [_ [_ [_ HI1]]]; destruct HPar2 as [_ [_ [_ HI2]]].
      split; intros [I [HC1 HC2]]; [apply HI1| apply HI2]; exists I; Col.
      }
    }
  }
Qed.

Lemma not_ex_forall_not_7 :
  forall (T : Type) (P : T -> T -> T -> T -> T -> T -> T -> Prop),
  ~(exists x1 : T, exists x2 : T, exists x3 : T,
    exists x4 : T, exists x5 : T, exists x6 : T,
    exists x7 :T, P x1 x2 x3 x4 x5 x6 x7) <->
  forall x1 : T, forall x2 : T, forall x3 : T,
  forall x4 : T, forall x5 : T, forall x6 : T,
  forall x7 : T, ~ P x1 x2 x3 x4 x5 x6 x7.
Proof.
intros; split; intro H1; intros; intro H2;
[apply H1; exists x1, x2, x3, x4, x5, x6, x7; auto|].
(* Goal: False *)
destruct H2 as [x1 [x2 [x3 [x4 [x5 [x6 [x7 H2]]]]]]].
(* Goal: False *)
apply (H1 x1 x2 x3 x4 x5 x6 x7); auto.
Qed.

Lemma playfair_quater__playfair :
  playfair_quater -> playfair_s_postulate.
Proof.
(* Goal: forall _ : playfair_quater, @playfair_s_postulate Tn *)
intros HP A1 A2 B1 B2 C1 C2 P HPar1 HP1 HPar2 HP2.
assert (H : playfair_quater <->
              forall A1 A2 B1 B2 C1 C2 P,
                ~ playfair_quater_qf A1 A2 B1 B2 C1 C2 P)
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
  by (apply not_ex_forall_not_7). rewrite H in HP; clear H.
assert (H : Col C1 B1 B2 /\ Col C2 B1 B2 <-> ~ ~ (Col C1 B1 B2 /\ Col C2 B1 B2))
  by (induction (col_dec C1 B1 B2); induction (col_dec C2 B1 B2); tauto).
(* Goal: and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
apply H; clear H; intro HNC; apply (HP A1 A2 B1 B2 C1 C2 P).
(* Goal: playfair_quater_qf A1 A2 B1 B2 C1 C2 P *)
repeat try (split; [assert_diffs; assumption|]).
(* Goal: and (not (and (@Col Tn A1 B1 B2) (@Col Tn A2 B1 B2))) (and (not (and (@Col Tn A1 C1 C2) (@Col Tn A2 C1 C2))) (and (not (and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2))) (and (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => not (and (not (and (@Col Tn A1 A2 I) (@Col Tn B1 B2 I))) (and (not (and (@Col Tn A1 B1 I) (@Col Tn A2 B2 I))) (not (and (@Col Tn A1 B2 I) (@Col Tn A2 B1 I))))))) (and (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => not (and (not (and (@Col Tn A1 A2 I) (@Col Tn C1 C2 I))) (and (not (and (@Col Tn A1 C1 I) (@Col Tn A2 C2 I))) (not (and (@Col Tn A1 C2 I) (@Col Tn A2 C1 I))))))) (and (not (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I A1 A2) (@Col Tn I B1 B2)))) (not (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I A1 A2) (@Col Tn I C1 C2))))))))) *)
assert (HNC1 : ~ Col A1 B1 B2).
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => not (and (not (and (@Col Tn A1 A2 I) (@Col Tn C1 C2 I))) (and (not (and (@Col Tn A1 C1 I) (@Col Tn A2 C2 I))) (not (and (@Col Tn A1 C2 I) (@Col Tn A2 C1 I)))))) *)
  {
(* Goal: not (@Col Tn A2 C1 C2) *)
  intro.
(* Goal: False *)
  assert (HA : A1 <> A2) by (assert_diffs; auto).
(* Goal: False *)
  assert (HB : B1 <> B2) by (assert_diffs; auto).
(* Goal: False *)
  assert (HC : C1 <> C2) by (assert_diffs; auto).
(* Goal: False *)
  apply (not_strict_par _ _ _ _ A1) in HPar1; Col; spliter.
(* Goal: False *)
  apply (not_strict_par _ _ _ _ P) in HPar2; spliter; try ColR.
(* Goal: False *)
  apply HNC; split; ColR.
  }
(* Goal: and (not (and (@Col Tn A1 B1 B2) (@Col Tn A2 B1 B2))) (and (not (and (@Col Tn A1 C1 C2) (@Col Tn A2 C1 C2))) (and (not (and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2))) (and (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => not (and (not (and (@Col Tn A1 A2 I) (@Col Tn B1 B2 I))) (and (not (and (@Col Tn A1 B1 I) (@Col Tn A2 B2 I))) (not (and (@Col Tn A1 B2 I) (@Col Tn A2 B1 I))))))) (and (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => not (and (not (and (@Col Tn A1 A2 I) (@Col Tn C1 C2 I))) (and (not (and (@Col Tn A1 C1 I) (@Col Tn A2 C2 I))) (not (and (@Col Tn A1 C2 I) (@Col Tn A2 C1 I))))))) (and (not (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I A1 A2) (@Col Tn I B1 B2)))) (not (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I A1 A2) (@Col Tn I C1 C2))))))))) *)
assert (HNC2 : ~ Col A2 B1 B2).
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => not (and (not (and (@Col Tn A1 A2 I) (@Col Tn C1 C2 I))) (and (not (and (@Col Tn A1 C1 I) (@Col Tn A2 C2 I))) (not (and (@Col Tn A1 C2 I) (@Col Tn A2 C1 I)))))) *)
  {
(* Goal: not (@Col Tn A2 C1 C2) *)
  intro.
(* Goal: False *)
  assert (HA : A1 <> A2) by (assert_diffs; auto).
(* Goal: False *)
  assert (HB : B1 <> B2) by (assert_diffs; auto).
(* Goal: False *)
  assert (HC : C1 <> C2) by (assert_diffs; auto).
(* Goal: False *)
  apply (not_strict_par _ _ _ _ A2) in HPar1; Col; spliter.
(* Goal: False *)
  apply (not_strict_par _ _ _ _ P) in HPar2; spliter; try ColR.
(* Goal: False *)
  apply HNC; split; ColR.
  }
(* Goal: and (not (and (@Col Tn A1 B1 B2) (@Col Tn A2 B1 B2))) (and (not (and (@Col Tn A1 C1 C2) (@Col Tn A2 C1 C2))) (and (not (and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2))) (and (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => not (and (not (and (@Col Tn A1 A2 I) (@Col Tn B1 B2 I))) (and (not (and (@Col Tn A1 B1 I) (@Col Tn A2 B2 I))) (not (and (@Col Tn A1 B2 I) (@Col Tn A2 B1 I))))))) (and (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => not (and (not (and (@Col Tn A1 A2 I) (@Col Tn C1 C2 I))) (and (not (and (@Col Tn A1 C1 I) (@Col Tn A2 C2 I))) (not (and (@Col Tn A1 C2 I) (@Col Tn A2 C1 I))))))) (and (not (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I A1 A2) (@Col Tn I B1 B2)))) (not (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I A1 A2) (@Col Tn I C1 C2))))))))) *)
assert (HNC3 : ~ Col A1 C1 C2).
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => not (and (not (and (@Col Tn A1 A2 I) (@Col Tn C1 C2 I))) (and (not (and (@Col Tn A1 C1 I) (@Col Tn A2 C2 I))) (not (and (@Col Tn A1 C2 I) (@Col Tn A2 C1 I)))))) *)
  {
(* Goal: not (@Col Tn A2 C1 C2) *)
  intro.
(* Goal: False *)
  assert (HA : A1 <> A2) by (assert_diffs; auto).
(* Goal: False *)
  assert (HB : B1 <> B2) by (assert_diffs; auto).
(* Goal: False *)
  assert (HC : C1 <> C2) by (assert_diffs; auto).
(* Goal: False *)
  apply (not_strict_par _ _ _ _ A1) in HPar2; Col; spliter.
(* Goal: False *)
  apply (not_strict_par _ _ _ _ P) in HPar1; spliter; try ColR.
(* Goal: False *)
  apply HNC; split; ColR.
  }
(* Goal: and (not (and (@Col Tn A1 B1 B2) (@Col Tn A2 B1 B2))) (and (not (and (@Col Tn A1 C1 C2) (@Col Tn A2 C1 C2))) (and (not (and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2))) (and (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => not (and (not (and (@Col Tn A1 A2 I) (@Col Tn B1 B2 I))) (and (not (and (@Col Tn A1 B1 I) (@Col Tn A2 B2 I))) (not (and (@Col Tn A1 B2 I) (@Col Tn A2 B1 I))))))) (and (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => not (and (not (and (@Col Tn A1 A2 I) (@Col Tn C1 C2 I))) (and (not (and (@Col Tn A1 C1 I) (@Col Tn A2 C2 I))) (not (and (@Col Tn A1 C2 I) (@Col Tn A2 C1 I))))))) (and (not (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I A1 A2) (@Col Tn I B1 B2)))) (not (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I A1 A2) (@Col Tn I C1 C2))))))))) *)
assert (HNC4 : ~ Col A2 C1 C2).
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => not (and (not (and (@Col Tn A1 A2 I) (@Col Tn C1 C2 I))) (and (not (and (@Col Tn A1 C1 I) (@Col Tn A2 C2 I))) (not (and (@Col Tn A1 C2 I) (@Col Tn A2 C1 I)))))) *)
  {
(* Goal: not (@Col Tn A2 C1 C2) *)
  intro.
(* Goal: False *)
  assert (HA : A1 <> A2) by (assert_diffs; auto).
(* Goal: False *)
  assert (HB : B1 <> B2) by (assert_diffs; auto).
(* Goal: False *)
  assert (HC : C1 <> C2) by (assert_diffs; auto).
(* Goal: False *)
  apply (not_strict_par _ _ _ _ A2) in HPar2; Col; spliter.
(* Goal: False *)
  apply (not_strict_par _ _ _ _ P) in HPar1; spliter; try ColR.
(* Goal: False *)
  apply HNC; split; ColR.
  }
apply par_symmetry in HPar1; apply (par_not_col_strict _ _ _ _ A1) in HPar1;
Col; apply par_strict_symmetry in HPar1; destruct HPar1 as [_ [_ [HCop1 HPar1]]].
apply par_symmetry in HPar2; apply (par_not_col_strict _ _ _ _ A1) in HPar2;
Col; apply par_strict_symmetry in HPar2; destruct HPar2 as [_ [_ [HCop2 HPar2]]].
(* Goal: and (not (and (@Col Tn A1 B1 B2) (@Col Tn A2 B1 B2))) (and (not (and (@Col Tn A1 C1 C2) (@Col Tn A2 C1 C2))) (and (not (and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2))) (and (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => not (and (not (and (@Col Tn A1 A2 I) (@Col Tn B1 B2 I))) (and (not (and (@Col Tn A1 B1 I) (@Col Tn A2 B2 I))) (not (and (@Col Tn A1 B2 I) (@Col Tn A2 B1 I))))))) (and (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => not (and (not (and (@Col Tn A1 A2 I) (@Col Tn C1 C2 I))) (and (not (and (@Col Tn A1 C1 I) (@Col Tn A2 C2 I))) (not (and (@Col Tn A1 C2 I) (@Col Tn A2 C1 I))))))) (and (not (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I A1 A2) (@Col Tn I B1 B2)))) (not (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I A1 A2) (@Col Tn I C1 C2))))))))) *)
repeat (split; try tauto).

(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => not (and (not (and (@Col Tn A1 A2 I) (@Col Tn C1 C2 I))) (and (not (and (@Col Tn A1 C1 I) (@Col Tn A2 C2 I))) (not (and (@Col Tn A1 C2 I) (@Col Tn A2 C1 I)))))) *)
  {
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => not (and (not (and (@Col Tn A1 A2 I) (@Col Tn B1 B2 I))) (and (not (and (@Col Tn A1 B1 I) (@Col Tn A2 B2 I))) (not (and (@Col Tn A1 B2 I) (@Col Tn A2 B1 I)))))) *)
  destruct HCop1 as [IAB HIAB].
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => not (and (not (and (@Col Tn A1 A2 I) (@Col Tn B1 B2 I))) (and (not (and (@Col Tn A1 B1 I) (@Col Tn A2 B2 I))) (not (and (@Col Tn A1 B2 I) (@Col Tn A2 B1 I)))))) *)
  exists IAB; intros [HIAB1 [HIAB2 HIAB3]].
  elim HIAB; clear HIAB; intro HIAB; [apply HIAB1|];
  try solve [spliter; split; Col].
  elim HIAB; clear HIAB; intro HIAB; [apply HIAB2|apply HIAB3];
  spliter; split; Col.
  }

(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => not (and (not (and (@Col Tn A1 A2 I) (@Col Tn C1 C2 I))) (and (not (and (@Col Tn A1 C1 I) (@Col Tn A2 C2 I))) (not (and (@Col Tn A1 C2 I) (@Col Tn A2 C1 I)))))) *)
  {
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => not (and (not (and (@Col Tn A1 A2 I) (@Col Tn C1 C2 I))) (and (not (and (@Col Tn A1 C1 I) (@Col Tn A2 C2 I))) (not (and (@Col Tn A1 C2 I) (@Col Tn A2 C1 I)))))) *)
  destruct HCop2 as [IAC HIAC].
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => not (and (not (and (@Col Tn A1 A2 I) (@Col Tn C1 C2 I))) (and (not (and (@Col Tn A1 C1 I) (@Col Tn A2 C2 I))) (not (and (@Col Tn A1 C2 I) (@Col Tn A2 C1 I)))))) *)
  exists IAC; intros [HIAC1 [HIAC2 HIAC3]].
  elim HIAC; clear HIAC; intro HIAC; [apply HIAC1|];
  try solve [spliter; split; Col].
  elim HIAC; clear HIAC; intro HIAC; [apply HIAC2|apply HIAC3];
  spliter; split; Col.
  }
Qed.

End par_trans_NID.