Require Export GeoCoq.Tarski_dev.Ch04_cong_bet.

Section T4_1.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma col_permutation_1 : forall A B C,Col A B C -> Col B C A.
Proof.
(* Goal: forall (A B C D A' B' C' D' : @Tpoint Tn) (_ : and (@Col Tn A B C) (and (@Cong_3 Tn A B C A' B' C') (and (@Cong Tn A D A' D') (@Cong Tn B D B' D')))) (_ : not (@eq (@Tpoint Tn) A B)), @Cong Tn C D C' D' *)
    unfold Col.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)), and (not (@Col Tn A B C)) (and (not (@Col Tn A C B)) (and (not (@Col Tn B A C)) (and (not (@Col Tn B C A)) (and (not (@Col Tn C A B)) (not (@Col Tn C B A)))))) *)
    intros.
(* Goal: @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => @Cong_3 Tn A B C A' B' C') *)
    intuition.
Qed.

Lemma col_permutation_2 : forall A B C, Col A B C -> Col C A B.
Proof.
(* Goal: forall (A B C D A' B' C' D' : @Tpoint Tn) (_ : and (@Col Tn A B C) (and (@Cong_3 Tn A B C A' B' C') (and (@Cong Tn A D A' D') (@Cong Tn B D B' D')))) (_ : not (@eq (@Tpoint Tn) A B)), @Cong Tn C D C' D' *)
    unfold Col.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)), and (not (@Col Tn A B C)) (and (not (@Col Tn A C B)) (and (not (@Col Tn B A C)) (and (not (@Col Tn B C A)) (and (not (@Col Tn C A B)) (not (@Col Tn C B A)))))) *)
    intros.
(* Goal: @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => @Cong_3 Tn A B C A' B' C') *)
    intuition.
Qed.

Lemma col_permutation_3 : forall A B C, Col A B C -> Col C B A.
Proof.
(* Goal: forall (A B C D A' B' C' D' : @Tpoint Tn) (_ : and (@Col Tn A B C) (and (@Cong_3 Tn A B C A' B' C') (and (@Cong Tn A D A' D') (@Cong Tn B D B' D')))) (_ : not (@eq (@Tpoint Tn) A B)), @Cong Tn C D C' D' *)
    unfold Col.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)), and (not (@Col Tn A B C)) (and (not (@Col Tn A C B)) (and (not (@Col Tn B A C)) (and (not (@Col Tn B C A)) (and (not (@Col Tn C A B)) (not (@Col Tn C B A)))))) *)
    intros.
(* Goal: @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => @Cong_3 Tn A B C A' B' C') *)
    intuition.
Qed.

Lemma col_permutation_4 : forall A B C, Col A B C -> Col B A C.
Proof.
(* Goal: forall (A B C D A' B' C' D' : @Tpoint Tn) (_ : and (@Col Tn A B C) (and (@Cong_3 Tn A B C A' B' C') (and (@Cong Tn A D A' D') (@Cong Tn B D B' D')))) (_ : not (@eq (@Tpoint Tn) A B)), @Cong Tn C D C' D' *)
    unfold Col.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)), and (not (@Col Tn A B C)) (and (not (@Col Tn A C B)) (and (not (@Col Tn B A C)) (and (not (@Col Tn B C A)) (and (not (@Col Tn C A B)) (not (@Col Tn C B A)))))) *)
    intros.
(* Goal: @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => @Cong_3 Tn A B C A' B' C') *)
    intuition.
Qed.

Lemma col_permutation_5 : forall A B C, Col A B C -> Col A C B.
Proof.
(* Goal: forall (A B C D A' B' C' D' : @Tpoint Tn) (_ : and (@Col Tn A B C) (and (@Cong_3 Tn A B C A' B' C') (and (@Cong Tn A D A' D') (@Cong Tn B D B' D')))) (_ : not (@eq (@Tpoint Tn) A B)), @Cong Tn C D C' D' *)
    unfold Col.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)), and (not (@Col Tn A B C)) (and (not (@Col Tn A C B)) (and (not (@Col Tn B A C)) (and (not (@Col Tn B C A)) (and (not (@Col Tn C A B)) (not (@Col Tn C B A)))))) *)
    intros.
(* Goal: @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => @Cong_3 Tn A B C A' B' C') *)
    intuition.
Qed.

End T4_1.

Hint Resolve bet_col col_permutation_1 col_permutation_2
col_permutation_3 col_permutation_4 col_permutation_5 : col.

Ltac Col := auto 3 with col.
Ltac Col5 := auto with col.

Section T4_2.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma not_col_permutation_1 :
 forall (A B C : Tpoint), ~ Col A B C -> ~ Col B C A.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)), and (not (@Col Tn A B C)) (and (not (@Col Tn A C B)) (and (not (@Col Tn B A C)) (and (not (@Col Tn B C A)) (and (not (@Col Tn C A B)) (not (@Col Tn C B A)))))) *)
    intros.
(* Goal: not (@Col Tn A C B) *)
    intro.
(* Goal: False *)
    apply H.
(* Goal: @Col Tn A B C *)
    Col.
Qed.

Lemma not_col_permutation_2 :
 forall (A B C : Tpoint), ~ Col A B C -> ~ Col C A B.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)), and (not (@Col Tn A B C)) (and (not (@Col Tn A C B)) (and (not (@Col Tn B A C)) (and (not (@Col Tn B C A)) (and (not (@Col Tn C A B)) (not (@Col Tn C B A)))))) *)
    intros.
(* Goal: not (@Col Tn A C B) *)
    intro.
(* Goal: False *)
    apply H.
(* Goal: @Col Tn A B C *)
    Col.
Qed.

Lemma not_col_permutation_3 :
 forall (A B C : Tpoint), ~ Col A B C -> ~ Col C B A.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)), and (not (@Col Tn A B C)) (and (not (@Col Tn A C B)) (and (not (@Col Tn B A C)) (and (not (@Col Tn B C A)) (and (not (@Col Tn C A B)) (not (@Col Tn C B A)))))) *)
    intros.
(* Goal: not (@Col Tn A C B) *)
    intro.
(* Goal: False *)
    apply H.
(* Goal: @Col Tn A B C *)
    Col.
Qed.

Lemma not_col_permutation_4 :
 forall (A B C : Tpoint), ~ Col A B C -> ~ Col B A C.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)), and (not (@Col Tn A B C)) (and (not (@Col Tn A C B)) (and (not (@Col Tn B A C)) (and (not (@Col Tn B C A)) (and (not (@Col Tn C A B)) (not (@Col Tn C B A)))))) *)
    intros.
(* Goal: not (@Col Tn A C B) *)
    intro.
(* Goal: False *)
    apply H.
(* Goal: @Col Tn A B C *)
    Col.
Qed.

Lemma not_col_permutation_5 :
 forall (A B C : Tpoint), ~ Col A B C -> ~ Col A C B.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)), and (not (@Col Tn A B C)) (and (not (@Col Tn A C B)) (and (not (@Col Tn B A C)) (and (not (@Col Tn B C A)) (and (not (@Col Tn C A B)) (not (@Col Tn C B A)))))) *)
    intros.
(* Goal: not (@Col Tn A C B) *)
    intro.
(* Goal: False *)
    apply H.
(* Goal: @Col Tn A B C *)
    Col.
Qed.

End T4_2.

Hint Resolve not_col_permutation_1 not_col_permutation_2
not_col_permutation_3 not_col_permutation_4 not_col_permutation_5 : col.

Section T4_3.

Context `{Tn:Tarski_neutral_dimensionless}.

(** This lemma is used by tactics for trying several permutations. *)
Lemma Col_cases :
 forall A B C,
 Col A B C \/ Col A C B \/ Col B A C \/
 Col B C A \/ Col C A B \/ Col C B A ->
 Col A B C.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)), and (not (@Col Tn A B C)) (and (not (@Col Tn A C B)) (and (not (@Col Tn B A C)) (and (not (@Col Tn B C A)) (and (not (@Col Tn C A B)) (not (@Col Tn C B A)))))) *)
    intros.
(* Goal: @Col Tn A B C *)
    decompose [or] H; Col.
Qed.

Lemma Col_perm :
 forall A B C,
 Col A B C ->
 Col A B C /\ Col A C B /\ Col B A C /\
 Col B C A /\ Col C A B /\ Col C B A.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)), and (not (@Col Tn A B C)) (and (not (@Col Tn A C B)) (and (not (@Col Tn B A C)) (and (not (@Col Tn B C A)) (and (not (@Col Tn C A B)) (not (@Col Tn C B A)))))) *)
    intros.
(* Goal: @Col Tn A B C *)
    repeat split; Col.
Qed.

Lemma col_trivial_1 : forall A B, Col A A B.
Proof.
(* Goal: forall (A B C D A' B' C' D' : @Tpoint Tn) (_ : and (@Col Tn A B C) (and (@Cong_3 Tn A B C A' B' C') (and (@Cong Tn A D A' D') (@Cong Tn B D B' D')))) (_ : not (@eq (@Tpoint Tn) A B)), @Cong Tn C D C' D' *)
    unfold Col.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)), and (not (@Col Tn A B C)) (and (not (@Col Tn A C B)) (and (not (@Col Tn B A C)) (and (not (@Col Tn B C A)) (and (not (@Col Tn C A B)) (not (@Col Tn C B A)))))) *)
    intros.
(* Goal: or (@Bet Tn A B B) (or (@Bet Tn B B A) (@Bet Tn B A B)) *)
    Between.
Qed.

Lemma col_trivial_2 : forall A B, Col A B B.
Proof.
(* Goal: forall (A B C D A' B' C' D' : @Tpoint Tn) (_ : and (@Col Tn A B C) (and (@Cong_3 Tn A B C A' B' C') (and (@Cong Tn A D A' D') (@Cong Tn B D B' D')))) (_ : not (@eq (@Tpoint Tn) A B)), @Cong Tn C D C' D' *)
    unfold Col.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)), and (not (@Col Tn A B C)) (and (not (@Col Tn A C B)) (and (not (@Col Tn B A C)) (and (not (@Col Tn B C A)) (and (not (@Col Tn C A B)) (not (@Col Tn C B A)))))) *)
    intros.
(* Goal: or (@Bet Tn A B B) (or (@Bet Tn B B A) (@Bet Tn B A B)) *)
    Between.
Qed.

Lemma col_trivial_3 : forall A B, Col A B A.
Proof.
(* Goal: forall (A B C D A' B' C' D' : @Tpoint Tn) (_ : and (@Col Tn A B C) (and (@Cong_3 Tn A B C A' B' C') (and (@Cong Tn A D A' D') (@Cong Tn B D B' D')))) (_ : not (@eq (@Tpoint Tn) A B)), @Cong Tn C D C' D' *)
    unfold Col.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)), and (not (@Col Tn A B C)) (and (not (@Col Tn A C B)) (and (not (@Col Tn B A C)) (and (not (@Col Tn B C A)) (and (not (@Col Tn C A B)) (not (@Col Tn C B A)))))) *)
    intros.
(* Goal: or (@Bet Tn A B B) (or (@Bet Tn B B A) (@Bet Tn B A B)) *)
    right;Between.
Qed.

End T4_3.

Hint Immediate col_trivial_1 col_trivial_2 col_trivial_3: col.

Section T4_4.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma l4_13 : forall A B C A' B' C',
 Col A B C -> Cong_3 A B C A' B' C' -> Col A' B' C'.
Proof.
(* Goal: forall (A B C D A' B' C' D' : @Tpoint Tn) (_ : and (@Col Tn A B C) (and (@Cong_3 Tn A B C A' B' C') (and (@Cong Tn A D A' D') (@Cong Tn B D B' D')))) (_ : not (@eq (@Tpoint Tn) A B)), @Cong Tn C D C' D' *)
    unfold Col.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)), and (not (@Col Tn A B C)) (and (not (@Col Tn A C B)) (and (not (@Col Tn B A C)) (and (not (@Col Tn B C A)) (and (not (@Col Tn C A B)) (not (@Col Tn C B A)))))) *)
    intros.
    decompose [or] H;
      eauto 6  using l4_6 with cong3.
Qed.

Lemma l4_14 : forall A B C A' B',
  Col A B C -> Cong A B A' B' -> exists C', Cong_3 A B C A' B' C'.
Proof.
(* Goal: forall (A B C D A' B' C' D' : @Tpoint Tn) (_ : and (@Col Tn A B C) (and (@Cong_3 Tn A B C A' B' C') (and (@Cong Tn A D A' D') (@Cong Tn B D B' D')))) (_ : not (@eq (@Tpoint Tn) A B)), @Cong Tn C D C' D' *)
    unfold Col.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)), and (not (@Col Tn A B C)) (and (not (@Col Tn A C B)) (and (not (@Col Tn B A C)) (and (not (@Col Tn B C A)) (and (not (@Col Tn C A B)) (not (@Col Tn C B A)))))) *)
    intros.
(* Goal: @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => @Cong_3 Tn A B C A' B' C') *)
    intuition.
(* Goal: @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => @Cong_3 Tn A B C A' B' C') *)
(* Goal: @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => @Cong_3 Tn A B C A' B' C') *)
(* Goal: @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => @Cong_3 Tn A B C A' B' C') *)
      prolong A' B' C' B C.
(* Goal: @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => @Cong_3 Tn A B C A' B' C') *)
      exists C'.
(* Goal: @Cong_3 Tn A B C A' B' C' *)
(* Goal: @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => @Cong_3 Tn A B C A' B' C') *)
(* Goal: @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => @Cong_3 Tn A B C A' B' C') *)
      assert (Cong A C A' C') by (eapply l2_11;eCong).
(* Goal: @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => @Cong_3 Tn A B C A' B' C') *)
      unfold Cong_3;intuition.
(* Goal: @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => @Cong_3 Tn A B C A' B' C') *)
(* Goal: @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => @Cong_3 Tn A B C A' B' C') *)
      assert (exists C', Bet A' C' B' /\ Cong_3 A C B A' C' B') by (eapply l4_5;Between).
(* Goal: @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => @Cong_3 Tn A B C A' B' C') *)
(* Goal: @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => @Cong_3 Tn A B C A' B' C') *)
      ex_and H1 C'.
(* Goal: @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => @Cong_3 Tn A B C A' B' C') *)
      exists C'.
(* Goal: @Cong_3 Tn A B C A' B' C' *)
(* Goal: @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => @Cong_3 Tn A B C A' B' C') *)
      auto with cong3.
(* Goal: @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => @Cong_3 Tn A B C A' B' C') *)
    prolong B' A' C' A C.
(* Goal: @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => @Cong_3 Tn A B C A' B' C') *)
    exists C'.
(* Goal: @Cong_3 Tn A B C A' B' C' *)
    assert (Cong B C B' C') by (eapply l2_11;eBetween;Cong).
(* Goal: @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => @Cong_3 Tn A B C A' B' C') *)
    unfold Cong_3;intuition.
Qed.

Lemma l4_16 : forall A B C D A' B' C' D',
   FSC A B C D A' B' C' D' -> A<>B -> Cong C D C' D'.
Proof.
(* Goal: forall (A B C D A' B' C' D' : @Tpoint Tn) (_ : @FSC Tn A B C D A' B' C' D') (_ : not (@eq (@Tpoint Tn) A B)), @Cong Tn C D C' D' *)
    unfold FSC.
(* Goal: forall (A B C D A' B' C' D' : @Tpoint Tn) (_ : and (@Col Tn A B C) (and (@Cong_3 Tn A B C A' B' C') (and (@Cong Tn A D A' D') (@Cong Tn B D B' D')))) (_ : not (@eq (@Tpoint Tn) A B)), @Cong Tn C D C' D' *)
    unfold Col.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)), and (not (@Col Tn A B C)) (and (not (@Col Tn A C B)) (and (not (@Col Tn B A C)) (and (not (@Col Tn B C A)) (and (not (@Col Tn C A B)) (not (@Col Tn C B A)))))) *)
    intros.
(* Goal: @Cong Tn C D C' D' *)
    decompose [or and] H; clear H.
(* Goal: @Cong Tn C D C' D' *)
(* Goal: @Cong Tn C D C' D' *)
(* Goal: @Cong Tn C D C' D' *)
      assert (Bet A' B' C') by (eapply l4_6;eauto).
(* Goal: @Cong Tn C D C' D' *)
(* Goal: @Cong Tn C D C' D' *)
(* Goal: @Cong Tn C D C' D' *)
      unfold Cong_3 in *; spliter.
(* Goal: @Cong Tn C D C' D' *)
(* Goal: @Cong Tn C D C' D' *)
(* Goal: @Cong Tn C D C' D' *)
      assert(OFSC A B C D A' B' C' D') by (unfold OFSC;repeat split; assumption).
(* Goal: @Cong Tn C D C' D' *)
(* Goal: @Cong Tn C D C' D' *)
(* Goal: @Cong Tn C D C' D' *)
      eapply five_segment_with_def; eauto.
(* Goal: @Cong Tn C D C' D' *)
(* Goal: @Cong Tn C D C' D' *)
      assert(Bet B' C' A') by (apply (l4_6 B C A B' C' A'); Cong;auto with cong3).
(* Goal: @Cong Tn C D C' D' *)
(* Goal: @Cong Tn C D C' D' *)
      apply (l4_2 B C A D B' C' A' D').
(* Goal: @IFSC Tn B C A D B' C' A' D' *)
(* Goal: @Cong Tn C D C' D' *)
      unfold IFSC; unfold Cong_3 in *; spliter; repeat split;Between;Cong.
(* Goal: @Cong Tn C D C' D' *)
    assert (Bet C' A' B') by (eapply (l4_6 C A B C' A' B'); auto with cong3).
(* Goal: @Cong Tn C D C' D' *)
    eapply (five_segment_with_def B A C D B' A'); unfold OFSC; unfold Cong_3 in *; spliter; repeat split; Between; Cong.
Qed.

Lemma l4_17 : forall A B C P Q,
  A<>B -> Col A B C -> Cong A P A Q -> Cong B P B Q -> Cong C P C Q.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)), and (not (@Col Tn A B C)) (and (not (@Col Tn A C B)) (and (not (@Col Tn B A C)) (and (not (@Col Tn B C A)) (and (not (@Col Tn C A B)) (not (@Col Tn C B A)))))) *)
    intros.
(* Goal: @Cong Tn C P C Q *)
    assert (FSC A B C P A B C Q) by (unfold FSC; unfold Cong_3;repeat split; Cong).
(* Goal: @Cong Tn C P C Q *)
    eapply l4_16; eauto.
Qed.

Lemma l4_18 : forall A B C C',
  A<>B -> Col A B C -> Cong A C A C' -> Cong B C B C' -> C=C'.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)), and (not (@Col Tn A B C)) (and (not (@Col Tn A C B)) (and (not (@Col Tn B A C)) (and (not (@Col Tn B C A)) (and (not (@Col Tn C A B)) (not (@Col Tn C B A)))))) *)
    intros.
(* Goal: @eq (@Tpoint Tn) C C' *)
    apply cong_identity with C.
(* Goal: @Cong Tn C C' C C *)
    apply (l4_17 A B); Cong.
Qed.

Lemma l4_19 : forall A B C C',
 Bet A C B -> Cong A C A C' -> Cong B C B C' -> C=C'.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)), and (not (@Col Tn A B C)) (and (not (@Col Tn A C B)) (and (not (@Col Tn B A C)) (and (not (@Col Tn B C A)) (and (not (@Col Tn C A B)) (not (@Col Tn C B A)))))) *)
    intros.
(* Goal: @eq (@Tpoint Tn) C C' *)
    induction (eq_dec_points A B).
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
      treat_equalities; reflexivity.
(* Goal: @eq (@Tpoint Tn) C C' *)
    apply (l4_18 A B); Cong.
(* Goal: @Col Tn A B C *)
    auto using bet_col with col.
Qed.

Lemma not_col_distincts : forall A B C ,
 ~ Col A B C ->
 ~ Col A B C /\ A <> B /\ B <> C /\ A <> C.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)), and (not (@Col Tn A B C)) (and (not (@Col Tn A C B)) (and (not (@Col Tn B A C)) (and (not (@Col Tn B C A)) (and (not (@Col Tn C A B)) (not (@Col Tn C B A)))))) *)
    intros.
(* Goal: @Col Tn A B C *)
    repeat split;(auto;intro); subst; apply H; Col.
Qed.

Lemma NCol_cases :
 forall A B C,
 ~ Col A B C \/ ~ Col A C B \/ ~ Col B A C \/
 ~ Col B C A \/ ~ Col C A B \/ ~ Col C B A ->
 ~ Col A B C.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)), and (not (@Col Tn A B C)) (and (not (@Col Tn A C B)) (and (not (@Col Tn B A C)) (and (not (@Col Tn B C A)) (and (not (@Col Tn C A B)) (not (@Col Tn C B A)))))) *)
    intros.
(* Goal: @Col Tn A B C *)
    decompose [or] H; Col.
Qed.

Lemma NCol_perm :
 forall A B C,
 ~ Col A B C ->
 ~ Col A B C /\ ~ Col A C B /\ ~ Col B A C /\
 ~ Col B C A /\ ~ Col C A B /\ ~ Col C B A.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (@Col Tn A B C)), and (not (@Col Tn A B C)) (and (not (@Col Tn A C B)) (and (not (@Col Tn B A C)) (and (not (@Col Tn B C A)) (and (not (@Col Tn C A B)) (not (@Col Tn C B A)))))) *)
    intros.
(* Goal: @Col Tn A B C *)
    repeat split; Col.
Qed.

Lemma col_cong_3_cong_3_eq : forall A B C A' B' C1 C2,
  A <>B -> Col A B C -> Cong_3 A B C A' B' C1 -> Cong_3 A B C A' B' C2 -> C1 = C2.
Proof.
(* Goal: forall (A B C A' B' C1 C2 : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) A B)) (_ : @Col Tn A B C) (_ : @Cong_3 Tn A B C A' B' C1) (_ : @Cong_3 Tn A B C A' B' C2), @eq (@Tpoint Tn) C1 C2 *)
intros A B C A' B' C1 C2 HAB HCol HCong1 HCong2.
apply l4_18 with A' B'; try apply l4_13 with A B C; Col;
(* Goal: @Cong Tn C D C' D' *)
(* Goal: @Cong Tn C D C' D' *)
(* Goal: @Cong Tn C D C' D' *)
unfold Cong_3 in *; spliter.
(* Goal: @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => @Cong_3 Tn A B C A' B' C') *)
  intro; treat_equalities; intuition.
(* Goal: @Cong Tn A' C1 A' C2 *)
(* Goal: @Cong Tn B' C1 B' C2 *)
  apply cong_transitivity with A C; Cong.
(* Goal: @Cong Tn B' C1 B' C2 *)
  apply cong_transitivity with B C; Cong.
Qed.

End T4_4.
