Require Export GeoCoq.Tarski_dev.Ch11_angles.

Section T12_1.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma par_reflexivity : forall A B, A<>B -> Par A B A B.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: @Par Tn A B B C *)
    unfold Par.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Par_strict Tn A B C D), and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) A D)) (and (not (@eq (@Tpoint Tn) B C)) (and (not (@eq (@Tpoint Tn) B D)) (not (@eq (@Tpoint Tn) C D)))))) *)
    unfold Par_strict.
(* Goal: or (@Bet Tn B P T) (@Bet Tn B T P) *)
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
    right.
(* Goal: and (not (@Col Tn B A C)) (and (not (@Col Tn D A C)) (@ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)))) *)
(* Goal: @TS Tn A C B D *)
    repeat split.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      assumption.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      assumption.
(* Goal: @Col Tn A A B *)
(* Goal: @Col Tn A C D *)
(* Goal: @Col Tn D T C *)
(* Goal: @Col Tn D T B *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)) *)
(* Goal: @TS Tn A C B D *)
      apply col_trivial_1.
(* Goal: @Col Tn B A B *)
    apply col_trivial_3.
Qed.

Lemma par_strict_irreflexivity : forall A B,
 ~ Par_strict A B A B.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
    intro.
(* Goal: and (@OS Tn A C B D) (@OS Tn B D A C) *)
    unfold Par_strict in H.
(* Goal: @Perp Tn A C B P *)
    spliter.
(* Goal: @Perp Tn A B P P' *)
(* Goal: @Perp Tn P Q P P' *)
(* Goal: @Col Tn P P Q *)
    apply H2.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A B) (@Col Tn X C D)) *)
(* Goal: @OS Tn B D A C *)
    exists A.
(* Goal: @Col Tn A A B *)
(* Goal: @Col Tn A C D *)
(* Goal: @Col Tn D T C *)
(* Goal: @Col Tn D T B *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)) *)
(* Goal: @TS Tn A C B D *)
    split; apply col_trivial_1.
Qed.

Lemma not_par_strict_id : forall A B C,
 ~ Par_strict A B A C.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
    intro.
(* Goal: and (@OS Tn A C B D) (@OS Tn B D A C) *)
    unfold Par_strict in H.
(* Goal: @Perp Tn A C B P *)
    spliter.
(* Goal: @Perp Tn A B P P' *)
(* Goal: @Perp Tn P Q P P' *)
(* Goal: @Col Tn P P Q *)
    apply H2.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A B) (@Col Tn X C D)) *)
(* Goal: @OS Tn B D A C *)
    exists A.
(* Goal: and (@Col Tn P A B) (@Col Tn P X Y) *)
(* Goal: False *)
    split; Col.
Qed.

Lemma par_id : forall A B C,
 Par A B A C -> Col A B C.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: @TS Tn A C B D *)
    unfold Par in H.
(* Goal: @TS Tn A C B D *)
    induction H.
(* Goal: and (@OS Tn A C B D) (@OS Tn B D A C) *)
      unfold Par_strict in H.
(* Goal: @Perp Tn A C B P *)
      spliter.
(* Goal: @TS Tn A C B D *)
      apply False_ind.
(* Goal: @Perp Tn A B P P' *)
(* Goal: @Perp Tn P Q P P' *)
(* Goal: @Col Tn P P Q *)
      apply H2.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A B) (@Col Tn X C D)) *)
(* Goal: @OS Tn B D A C *)
      exists A.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
      Col.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
    spliter;Col.
Qed.

Lemma par_strict_not_col_1 : forall A B C D,
 Par_strict A B C D  -> ~ Col A B C.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: @Par_strict Tn B A C D *)
(* Goal: or (@Par_strict Tn B A C D) (and (not (@eq (@Tpoint Tn) B A)) (and (not (@eq (@Tpoint Tn) C D)) (and (@Col Tn B C D) (@Col Tn A C D)))) *)
    unfold Par_strict in *.
(* Goal: @Perp Tn A C B P *)
    spliter.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
    intro.
(* Goal: @Perp Tn A B P P' *)
(* Goal: @Perp Tn P Q P P' *)
(* Goal: @Col Tn P P Q *)
    apply H2.
(* Goal: @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => and (@Midpoint Tn T A C') (@Cong Tn B A B C')) *)
(* Goal: @Perp Tn A C B P *)
    exists C.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
    split;Col.
Qed.

Lemma par_strict_not_col_2 : forall A B C D,
 Par_strict A B C D  -> ~ Col B C D.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: @Par_strict Tn B A C D *)
(* Goal: or (@Par_strict Tn B A C D) (and (not (@eq (@Tpoint Tn) B A)) (and (not (@eq (@Tpoint Tn) C D)) (and (@Col Tn B C D) (@Col Tn A C D)))) *)
    unfold Par_strict in *.
(* Goal: @Perp Tn A C B P *)
    spliter.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
    intro.
(* Goal: @Perp Tn A B P P' *)
(* Goal: @Perp Tn P Q P P' *)
(* Goal: @Col Tn P P Q *)
    apply H2.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A B) (@Col Tn X C D)) *)
(* Goal: not (@TS Tn B D A C) *)
    exists B.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
    split;Col.
Qed.

Lemma par_strict_not_col_3 : forall A B C D,
 Par_strict A B C D  -> ~ Col C D A.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: @Par_strict Tn B A C D *)
(* Goal: or (@Par_strict Tn B A C D) (and (not (@eq (@Tpoint Tn) B A)) (and (not (@eq (@Tpoint Tn) C D)) (and (@Col Tn B C D) (@Col Tn A C D)))) *)
    unfold Par_strict in *.
(* Goal: @Perp Tn A C B P *)
    spliter.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
    intro.
(* Goal: @Perp Tn A B P P' *)
(* Goal: @Perp Tn P Q P P' *)
(* Goal: @Col Tn P P Q *)
    apply H2.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A B) (@Col Tn X C D)) *)
(* Goal: @OS Tn B D A C *)
    exists A.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
    split;Col.
Qed.

Lemma par_strict_not_col_4 : forall A B C D,
 Par_strict A B C D  -> ~ Col A B D.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: @Par_strict Tn B A C D *)
(* Goal: or (@Par_strict Tn B A C D) (and (not (@eq (@Tpoint Tn) B A)) (and (not (@eq (@Tpoint Tn) C D)) (and (@Col Tn B C D) (@Col Tn A C D)))) *)
    unfold Par_strict in *.
(* Goal: @Perp Tn A C B P *)
    spliter.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
    intro.
(* Goal: @Perp Tn A B P P' *)
(* Goal: @Perp Tn P Q P P' *)
(* Goal: @Col Tn P P Q *)
    apply H2.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A B) (@Col Tn X C D)) *)
(* Goal: not (@Col Tn C B D) *)
(* Goal: not (@TS Tn B D A C) *)
    exists D.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
    split;Col.
Qed.

Lemma par_strict_not_cols : forall A B C D,
 Par_strict A B C D -> ~ Col A B C /\ ~ Col B C D /\ ~ Col C D A /\ ~ Col A B D.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: and (not (@Col Tn B A C)) (and (not (@Col Tn D A C)) (@ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)))) *)
(* Goal: @TS Tn A C B D *)
    repeat split.
(* Goal: not (@Col Tn A B C) *)
(* Goal: not (@Col Tn B C D) *)
(* Goal: not (@Col Tn C D A) *)
(* Goal: not (@Col Tn A B D) *)
    apply par_strict_not_col_1 with D, H.
(* Goal: not (@Col Tn B C D) *)
(* Goal: not (@Col Tn C D A) *)
(* Goal: not (@Col Tn A B D) *)
    apply (par_strict_not_col_2 A), H.
(* Goal: not (@Col Tn C D A) *)
(* Goal: not (@Col Tn A B D) *)
    apply par_strict_not_col_3 with B, H.
(* Goal: not (@Col Tn A B D) *)
    apply par_strict_not_col_4 with C, H.
Qed.

Lemma par_id_1 : forall A B C,
 Par A B A C -> Col B A C.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: @Col Tn C A B *)
    assert (H1 := par_id A B C H).
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
    Col.
Qed.

Lemma par_id_2 : forall A B C,
 Par A B A C -> Col B C A.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: @Col Tn C A B *)
    assert (H1 := par_id A B C H).
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
    Col.
Qed.

Lemma par_id_3 : forall A B C,
 Par A B A C -> Col A C B.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: @Col Tn C A B *)
    assert (H1 := par_id A B C H).
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
    Col.
Qed.

Lemma par_id_4 : forall A B C,
 Par A B A C -> Col C B A.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: @Col Tn C A B *)
    assert (H1 := par_id A B C H).
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
    Col.
Qed.


Lemma par_id_5 : forall A B C,
 Par A B A C -> Col C A B.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: @Col Tn C A B *)
    assert (H1 := par_id A B C H).
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
    Col.
Qed.

Lemma par_strict_symmetry :forall A B C D,
 Par_strict A B C D -> Par_strict C D A B.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Par_strict Tn A B C D), and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) A D)) (and (not (@eq (@Tpoint Tn) B C)) (and (not (@eq (@Tpoint Tn) B D)) (not (@eq (@Tpoint Tn) C D)))))) *)
    unfold Par_strict.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: @Perp Tn A C B P *)
    spliter.
(* Goal: and (not (@Col Tn B A C)) (and (not (@Col Tn D A C)) (@ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)))) *)
(* Goal: @TS Tn A C B D *)
    repeat split.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      assumption.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      assumption.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      apply coplanar_perm_16;assumption.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
    intro.
(* Goal: @Perp Tn A B P P' *)
(* Goal: @Perp Tn P Q P P' *)
(* Goal: @Col Tn P P Q *)
    apply H2.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A B) (@Col Tn X C D)) *)
(* Goal: or (@Par_strict Tn B A C D) (and (not (@eq (@Tpoint Tn) B A)) (and (not (@eq (@Tpoint Tn) C D)) (and (@Col Tn B C D) (@Col Tn A C D)))) *)
    ex_and H3 X.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A B) (@Col Tn X C D)) *)
(* Goal: @Bet Tn B T D *)
(* Goal: @TS Tn A C B D *)
    exists X.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
    split; assumption.
Qed.

Lemma par_symmetry :forall A B C D,
 Par A B C D -> Par C D A B.
Proof.
(* Goal: @Par Tn A B B C *)
    unfold Par.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: @TS Tn A C B D *)
    induction H.
(* Goal: or (@Bet Tn B P T) (@Bet Tn B T P) *)
(* Goal: or (@Bet Tn B P T) (@Bet Tn B T P) *)
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
      left.
(* Goal: @Par_strict Tn C D A B *)
      apply par_strict_symmetry.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      assumption.
(* Goal: @Perp Tn A C B P *)
    spliter.
(* Goal: or (@Bet Tn B P T) (@Bet Tn B T P) *)
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
    right.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
    repeat split;try assumption.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
      eapply (col_transitivity_1 _ D);Col.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
    eapply (col_transitivity_1 _ C);Col.
Qed.

Lemma par_left_comm : forall A B C D,
 Par A B C D -> Par B A C D.
Proof.
(* Goal: @Par Tn A B B C *)
    unfold Par.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: @TS Tn A C B D *)
    induction H.
(* Goal: or (@Bet Tn B P T) (@Bet Tn B T P) *)
(* Goal: or (@Bet Tn B P T) (@Bet Tn B T P) *)
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
      left.
(* Goal: @Par_strict Tn B A C D *)
(* Goal: or (@Par_strict Tn B A C D) (and (not (@eq (@Tpoint Tn) B A)) (and (not (@eq (@Tpoint Tn) C D)) (and (@Col Tn B C D) (@Col Tn A C D)))) *)
      unfold Par_strict in *.
(* Goal: @Perp Tn A C B P *)
      spliter.
(* Goal: and (not (@Col Tn B A C)) (and (not (@Col Tn D A C)) (@ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)))) *)
(* Goal: @TS Tn A C B D *)
      repeat split.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
        auto.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
        assumption.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
        apply coplanar_perm_6;assumption.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
      intro.
(* Goal: @Perp Tn A B P P' *)
(* Goal: @Perp Tn P Q P P' *)
(* Goal: @Col Tn P P Q *)
      apply H2.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A B) (@Col Tn X C D)) *)
(* Goal: or (@Par_strict Tn B A C D) (and (not (@eq (@Tpoint Tn) B A)) (and (not (@eq (@Tpoint Tn) C D)) (and (@Col Tn B C D) (@Col Tn A C D)))) *)
      ex_and H3 X.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A B) (@Col Tn X C D)) *)
(* Goal: @Bet Tn B T D *)
(* Goal: @TS Tn A C B D *)
      exists X.
(* Goal: and (@Col Tn P A B) (@Col Tn P C D) *)
(* Goal: False *)
      Col5.
(* Goal: or (@Bet Tn B P T) (@Bet Tn B T P) *)
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
    right.
(* Goal: @Perp Tn A C B P *)
    spliter.
(* Goal: and (@Col Tn P A B) (@Col Tn P C D) *)
(* Goal: False *)
    Col5.
Qed.

Lemma par_right_comm : forall A B C D,
 Par A B C D -> Par A B D C.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: @Par Tn A B D C *)
    apply par_symmetry in H.
(* Goal: @Par Tn E F C D *)
    apply par_symmetry.
(* Goal: @Par Tn B A D C *)
    apply par_left_comm.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
    assumption.
Qed.

Lemma par_comm : forall A B C D,
 Par A B C D -> Par B A D C.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: @Par Tn B A D C *)
    apply par_left_comm.
(* Goal: @Par Tn A B P x *)
    apply par_right_comm.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
    assumption.
Qed.

Lemma par_strict_left_comm : forall A B C D,
 Par_strict A B C D -> Par_strict B A C D.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Par_strict Tn A B C D), and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) A D)) (and (not (@eq (@Tpoint Tn) B C)) (and (not (@eq (@Tpoint Tn) B D)) (not (@eq (@Tpoint Tn) C D)))))) *)
    unfold Par_strict.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) D C)) (and (@Coplanar Tn A B D C) (not (@ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A B) (@Col Tn X D C)))))) *)
    decompose [and] H;clear H.
(* Goal: and (not (@Col Tn B A C)) (and (not (@Col Tn D A C)) (@ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)))) *)
(* Goal: @TS Tn A C B D *)
    repeat split.
(* Goal: and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) C D)) *)
      intuition.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      assumption.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      apply coplanar_perm_6;assumption.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
    intro.
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
    apply H4.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A B) (@Col Tn X C D)) *)
    destruct H as [X [HCol1 HCol2]].
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
    exists X; Col.
Qed.

Lemma par_strict_right_comm : forall A B C D,
 Par_strict A B C D -> Par_strict A B D C.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Par_strict Tn A B C D), and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) A D)) (and (not (@eq (@Tpoint Tn) B C)) (and (not (@eq (@Tpoint Tn) B D)) (not (@eq (@Tpoint Tn) C D)))))) *)
    unfold Par_strict.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) D C)) (and (@Coplanar Tn A B D C) (not (@ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A B) (@Col Tn X D C)))))) *)
    decompose [and] H;clear H.
(* Goal: and (not (@Col Tn B A C)) (and (not (@Col Tn D A C)) (@ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)))) *)
(* Goal: @TS Tn A C B D *)
    repeat split.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      assumption.
(* Goal: and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) C D)) *)
      intuition.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      apply coplanar_perm_1;assumption.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
    intro.
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
    apply H4.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A B) (@Col Tn X C D)) *)
    destruct H as [X [HCol1 HCol2]].
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
    exists X; Col.
Qed.

Lemma par_strict_comm : forall A B C D,
 Par_strict A B C D -> Par_strict B A D C.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: @Par_strict Tn B A D C *)
    apply par_strict_left_comm in H.
(* Goal: @Par_strict Tn B A D C *)
    apply par_strict_right_comm.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
    assumption.
Qed.

Lemma par_strict_neq1 : forall A B C D, Par_strict A B C D -> A <> B.
Proof. unfold Par_strict; intros; spliter; auto. Qed.

Lemma par_strict_neq2 : forall A B C D, Par_strict A B C D -> C <> D.
Proof. unfold Par_strict; intros; spliter; auto. Qed.

Lemma par_neq1 : forall A B C D, Par A B C D -> A <> B.
Proof. unfold Par, Par_strict; intros; induction H; spliter; auto. Qed.

Lemma par_neq2 : forall A B C D, Par A B C D -> C <> D.
Proof. unfold Par, Par_strict; intros; induction H; spliter; auto. Qed.

End T12_1.

Ltac assert_diffs :=
repeat
 match goal with
      | H:(~Col ?X1 ?X2 ?X3) |- _ =>
      let h := fresh in
      not_exist_hyp3 X1 X2 X1 X3 X2 X3;
      assert (h := not_col_distincts X1 X2 X3 H);decompose [and] h;clear h;clean_reap_hyps

      | H:(~Bet ?X1 ?X2 ?X3) |- _ =>
      let h := fresh in
      not_exist_hyp2 X1 X2 X2 X3;
      assert (h := not_bet_distincts X1 X2 X3 H);decompose [and] h;clear h;clean_reap_hyps
      | H:Bet ?A ?B ?C, H2 : ?A <> ?B |-_ =>
      let T:= fresh in (not_exist_hyp_comm A C);
        assert (T:= bet_neq12__neq A B C H H2);clean_reap_hyps
      | H:Bet ?A ?B ?C, H2 : ?B <> ?A |-_ =>
      let T:= fresh in (not_exist_hyp_comm A C);
        assert (T:= bet_neq21__neq A B C H H2);clean_reap_hyps
      | H:Bet ?A ?B ?C, H2 : ?B <> ?C |-_ =>
      let T:= fresh in (not_exist_hyp_comm A C);
        assert (T:= bet_neq23__neq A B C H H2);clean_reap_hyps
      | H:Bet ?A ?B ?C, H2 : ?C <> ?B |-_ =>
      let T:= fresh in (not_exist_hyp_comm A C);
        assert (T:= bet_neq32__neq A B C H H2);clean_reap_hyps

      | H:Cong ?A ?B ?C ?D, H2 : ?A <> ?B |-_ =>
      let T:= fresh in (not_exist_hyp_comm C D);
        assert (T:= cong_diff A B C D H2 H);clean_reap_hyps
      | H:Cong ?A ?B ?C ?D, H2 : ?B <> ?A |-_ =>
      let T:= fresh in (not_exist_hyp_comm C D);
        assert (T:= cong_diff_2 A B C D H2 H);clean_reap_hyps
      | H:Cong ?A ?B ?C ?D, H2 : ?C <> ?D |-_ =>
      let T:= fresh in (not_exist_hyp_comm A B);
        assert (T:= cong_diff_3 A B C D H2 H);clean_reap_hyps
      | H:Cong ?A ?B ?C ?D, H2 : ?D <> ?C |-_ =>
      let T:= fresh in (not_exist_hyp_comm A B);
        assert (T:= cong_diff_4 A B C D H2 H);clean_reap_hyps

      | H:Le ?A ?B ?C ?D, H2 : ?A <> ?B |-_ =>
      let T:= fresh in (not_exist_hyp_comm C D);
        assert (T:= le_diff A B C D H2 H);clean_reap_hyps
      | H:Le ?A ?B ?C ?D, H2 : ?B <> ?A |-_ =>
      let T:= fresh in (not_exist_hyp_comm C D);
        assert (T:= le_diff A B C D (swap_diff B A H2) H);clean_reap_hyps
      | H:Lt ?A ?B ?C ?D |-_ =>
      let T:= fresh in (not_exist_hyp_comm C D);
        assert (T:= lt_diff A B C D H);clean_reap_hyps

      | H:Midpoint ?I ?A ?B, H2 : ?A<>?B |- _ =>
      let T:= fresh in (not_exist_hyp2 I B I A);
       assert (T:= midpoint_distinct_1 I A B H2 H);
       decompose [and] T;clear T;clean_reap_hyps
      | H:Midpoint ?I ?A ?B, H2 : ?B<>?A |- _ =>
      let T:= fresh in (not_exist_hyp2 I B I A);
       assert (T:= midpoint_distinct_1 I A B (swap_diff B A H2) H);
       decompose [and] T;clear T;clean_reap_hyps

      | H:Midpoint ?I ?A ?B, H2 : ?I<>?A |- _ =>
      let T:= fresh in (not_exist_hyp2 I B A B);
       assert (T:= midpoint_distinct_2 I A B H2 H);
       decompose [and] T;clear T;clean_reap_hyps
      | H:Midpoint ?I ?A ?B, H2 : ?A<>?I |- _ =>
      let T:= fresh in (not_exist_hyp2 I B A B);
       assert (T:= midpoint_distinct_2 I A B (swap_diff A I H2) H);
       decompose [and] T;clear T;clean_reap_hyps

      | H:Midpoint ?I ?A ?B, H2 : ?I<>?B |- _ =>
      let T:= fresh in (not_exist_hyp2 I A A B);
       assert (T:= midpoint_distinct_3 I A B H2 H);
       decompose [and] T;clear T;clean_reap_hyps
      | H:Midpoint ?I ?A ?B, H2 : ?B<>?I |- _ =>
      let T:= fresh in (not_exist_hyp2 I A A B);
       assert (T:= midpoint_distinct_3 I A B (swap_diff B I H2) H);
       decompose [and] T;clear T;clean_reap_hyps

      | H:Per ?A ?B ?C, H2 : ?A<>?B |- _ =>
      let T:= fresh in (not_exist_hyp_comm A C);
        assert (T:= per_distinct A B C H H2); clean_reap_hyps
      | H:Per ?A ?B ?C, H2 : ?B<>?A |- _ =>
      let T:= fresh in (not_exist_hyp_comm A C);
        assert (T:= per_distinct A B C H (swap_diff B A H2)); clean_reap_hyps
      | H:Per ?A ?B ?C, H2 : ?B<>?C |- _ =>
      let T:= fresh in (not_exist_hyp_comm A C);
        assert (T:= per_distinct_1 A B C H H2); clean_reap_hyps
      | H:Per ?A ?B ?C, H2 : ?C<>?B |- _ =>
      let T:= fresh in (not_exist_hyp_comm A C);
        assert (T:= per_distinct_1 A B C H (swap_diff C B H2)); clean_reap_hyps

      | H:Perp ?A ?B ?C ?D |- _ =>
      let T:= fresh in (not_exist_hyp2 A B C D);
       assert (T:= perp_distinct A B C D H);
       decompose [and] T;clear T;clean_reap_hyps
      | H:Perp_at ?X ?A ?B ?C ?D |- _ =>
      let T:= fresh in (not_exist_hyp2 A B C D);
       assert (T:= perp_in_distinct X A B C D H);
       decompose [and] T;clear T;clean_reap_hyps
      | H:Out ?A ?B ?C |- _ =>
      let T:= fresh in (not_exist_hyp2 A B A C);
       assert (T:= out_distinct A B C H);
       decompose [and] T;clear T;clean_reap_hyps

      | H:TS ?A ?B ?C ?D |- _ =>
      let h := fresh in
      not_exist_hyp6 A B A C A D B C B D C D;
      assert (h := ts_distincts A B C D H);decompose [and] h;clear h;clean_reap_hyps
      | H:OS ?A ?B ?C ?D |- _ =>
      let h := fresh in
      not_exist_hyp5 A B A C A D B C B D;
      assert (h := os_distincts A B C D H);decompose [and] h;clear h;clean_reap_hyps
      | H:~ Coplanar ?A ?B ?C ?D |- _ =>
      let h := fresh in
      not_exist_hyp6 A B A C A D B C B D C D;
      assert (h := ncop_distincts A B C D H);decompose [and] h;clear h;clean_reap_hyps

      | H:CongA ?A ?B ?C ?A' ?B' ?C' |- _ =>
      let T:= fresh in (not_exist_hyp_comm A B);
        assert (T:= conga_diff1 A B C A' B' C' H);clean_reap_hyps
      | H:CongA ?A ?B ?C ?A' ?B' ?C' |- _ =>
      let T:= fresh in (not_exist_hyp_comm B C);
        assert (T:= conga_diff2 A B C A' B' C' H);clean_reap_hyps
      | H:CongA ?A ?B ?C ?A' ?B' ?C' |- _ =>
      let T:= fresh in (not_exist_hyp_comm A' B');
        assert (T:= conga_diff45 A B C A' B' C' H);clean_reap_hyps
      | H:CongA ?A ?B ?C ?A' ?B' ?C' |- _ =>
      let T:= fresh in (not_exist_hyp_comm B' C');
        assert (T:= conga_diff56 A B C A' B' C' H);clean_reap_hyps

      | H:(InAngle ?P ?A ?B ?C) |- _ =>
      let h := fresh in
      not_exist_hyp3 A B C B P B;
      assert (h := inangle_distincts A B C P H);decompose [and] h;clear h;clean_reap_hyps
      | H:LeA ?A ?B ?C ?D ?E ?F |- _ =>
      let h := fresh in
      not_exist_hyp4 A B B C D E E F;
      assert (h := lea_distincts A B C D E F H);decompose [and] h;clear h;clean_reap_hyps
      | H:LtA ?A ?B ?C ?D ?E ?F |- _ =>
      let h := fresh in
      not_exist_hyp4 A B B C D E E F;
      assert (h := lta_distincts A B C D E F H);decompose [and] h;clear h;clean_reap_hyps
      | H:(Acute ?A ?B ?C) |- _ =>
      let h := fresh in
      not_exist_hyp2 A B B C;
      assert (h := acute_distincts A B C H);decompose [and] h;clear h;clean_reap_hyps
      | H:(Obtuse ?A ?B ?C) |- _ =>
      let h := fresh in
      not_exist_hyp2 A B B C;
      assert (h := obtuse_distincts A B C H);decompose [and] h;clear h;clean_reap_hyps
      | H:SuppA ?A ?B ?C ?D ?E ?F |- _ =>
      let h := fresh in
      not_exist_hyp4 A B B C D E E F;
      assert (h := suppa_distincts A B C D E F H);decompose [and] h;clear h;clean_reap_hyps

      | H:(Orth_at ?X ?A ?B ?C ?U ?V) |- _ =>
      let h := fresh in
      not_exist_hyp4 A B A C B C U V;
      assert (h := orth_at_distincts A B C U V X H);decompose [and] h;clear h;clean_reap_hyps
      | H:(Orth ?A ?B ?C ?U ?V) |- _ =>
      let h := fresh in
      not_exist_hyp4 A B A C B C U V;
      assert (h := orth_distincts A B C U V H);decompose [and] h;clear h;clean_reap_hyps

      | H:Par ?A ?B ?C ?D |- _ =>
      let T:= fresh in (not_exist_hyp_comm A B);
        assert (T:= par_neq1 A B C D H);clean_reap_hyps
      | H:Par ?A ?B ?C ?D |- _ =>
      let T:= fresh in (not_exist_hyp_comm C D);
        assert (T:= par_neq2 A B C D H);clean_reap_hyps
      | H:Par_strict ?A ?B ?C ?D |- _ =>
      let T:= fresh in (not_exist_hyp_comm A B);
        assert (T:= par_strict_neq1 A B C D H);clean_reap_hyps
      | H:Par_strict ?A ?B ?C ?D |- _ =>
      let T:= fresh in (not_exist_hyp_comm C D);
        assert (T:= par_strict_neq2 A B C D H);clean_reap_hyps
 end.

Ltac assert_ncols :=
repeat
  match goal with
      | H:OS ?A ?B ?X ?Y |- _ =>
     not_exist_hyp_perm_ncol A B X;assert (~ Col A B X) by (apply(one_side_not_col123 A B X Y);finish)

      | H:OS ?A ?B ?X ?Y |- _ =>
     not_exist_hyp_perm_ncol A B Y;assert (~ Col A B Y) by (apply(one_side_not_col124 A B X Y);finish)

      | H:TS ?A ?B ?X ?Y |- _ =>
     not_exist_hyp_perm_ncol A B X;assert (~ Col A B X) by (apply(two_sides_not_col A B X Y);finish)

      | H:TS ?A ?B ?X ?Y |- _ =>
     not_exist_hyp_perm_ncol A B Y;assert (~ Col A B Y) by (apply(two_sides_not_col A B Y X);finish)

      | H:~ Coplanar ?A ?B ?C ?D |- _ =>
      let h := fresh in
      not_exist_hyp_perm4 A B C D;
      assert (h := ncop__ncols A B C D H);decompose [and] h;clear h;clean_reap_hyps

      | H:Par_strict ?A ?B ?C ?D |- _ =>
      let h := fresh in
      not_exist_hyp_perm4 A B C D;
      assert (h := par_strict_not_cols A B C D H);decompose [and] h;clear h;clean_reap_hyps
  end.


Hint Resolve
 par_reflexivity par_strict_irreflexivity
 par_strict_symmetry par_strict_comm par_strict_right_comm par_strict_left_comm
 par_symmetry par_comm par_right_comm par_left_comm : par.

Hint Resolve par_strict_not_col_1 par_strict_not_col_2
             par_strict_not_col_3 par_strict_not_col_4 : col.

Ltac Par := eauto with par.

Section T12_2.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma Par_cases :
  forall A B C D,
  Par A B C D \/ Par B A C D \/ Par A B D C \/ Par B A D C \/
  Par C D A B \/ Par C D B A \/ Par D C A B \/ Par D C B A ->
  Par A B C D.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: @Par Tn A B A B *)
(* Goal: @Col Tn P A B *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (not (@eq (@Tpoint Tn) C D)) (and (@Par Tn A B C D) (@Col Tn P C D)))) *)
    decompose [or]  H;Par.
Qed.

Lemma Par_perm :
  forall A B C D,
  Par A B C D ->
  Par A B C D /\ Par B A C D /\ Par A B D C /\ Par B A D C /\
  Par C D A B /\ Par C D B A /\ Par D C A B /\ Par D C B A.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: and (@Par Tn A B C D) (and (@Par Tn B A C D) (and (@Par Tn A B D C) (and (@Par Tn B A D C) (and (@Par Tn C D A B) (and (@Par Tn C D B A) (and (@Par Tn D C A B) (@Par Tn D C B A))))))) *)
    do 7 (split; Par).
Qed.

Lemma Par_strict_cases :
  forall A B C D,
  Par_strict A B C D \/ Par_strict B A C D \/ Par_strict A B D C \/ Par_strict B A D C \/
  Par_strict C D A B \/ Par_strict C D B A \/ Par_strict D C A B \/ Par_strict D C B A ->
  Par_strict A B C D.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
    decompose [or]  H; eauto with par.
Qed.

Lemma Par_strict_perm :
  forall A B C D,
  Par_strict A B C D ->
  Par_strict A B C D /\ Par_strict B A C D /\ Par_strict A B D C /\ Par_strict B A D C /\
  Par_strict C D A B /\ Par_strict C D B A /\ Par_strict D C A B /\ Par_strict D C B A.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: and (@Par Tn A B C D) (and (@Par Tn B A C D) (and (@Par Tn A B D C) (and (@Par Tn B A D C) (and (@Par Tn C D A B) (and (@Par Tn C D B A) (and (@Par Tn D C A B) (@Par Tn D C B A))))))) *)
    do 7 (split; Par).
Qed.

End T12_2.

Section T12_2'.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma l12_6 : forall A B C D,
 Par_strict A B C D -> OS A B C D.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: and (@OS Tn A C B D) (@OS Tn B D A C) *)
    unfold Par_strict in H.
(* Goal: @Perp Tn A C B P *)
    spliter.
(* Goal: @OS Tn A B C D *)
    assert(HH:= cop__not_two_sides_one_side A B C D).
(* Goal: @OS Tn A B C D *)
    apply HH.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      assumption.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
      intro.
(* Goal: @Perp Tn A B P P' *)
(* Goal: @Perp Tn P Q P P' *)
(* Goal: @Col Tn P P Q *)
      apply H2.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
      exists C;Col.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
      intro.
(* Goal: @Perp Tn A B P P' *)
(* Goal: @Perp Tn P Q P P' *)
(* Goal: @Col Tn P P Q *)
      apply H2.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
      exists D;Col.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
    intro.
(* Goal: @Perp Tn A B P P' *)
(* Goal: @Perp Tn P Q P P' *)
(* Goal: @Col Tn P P Q *)
    apply H2.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A B) (@Col Tn X C D)) *)
    unfold TS in H3.
(* Goal: @Perp Tn A C B P *)
    spliter.
(* Goal: @Perp Tn A C B P *)
    ex_and H5 T.
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)) *)
(* Goal: @TS Tn A C B D *)
    exists T.
(* Goal: and (@Col Tn T A B) (@Col Tn T C D) *)
    eauto using bet_col with col.
Qed.

Lemma pars__os3412 : forall A B C D,
 Par_strict A B C D -> OS C D A B.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: @OS Tn C D A B *)
    apply l12_6.
(* Goal: @Par_strict Tn C D A B *)
    apply par_strict_symmetry.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
    assumption.
Qed.

Lemma perp_dec : forall A B C D, Perp A B C D \/ ~ Perp A B C D.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: or (@Perp Tn A B C D) (not (@Perp Tn A B C D)) *)
    induction (col_dec A B C).
(* Goal: or (@Perp Tn A B C D) (not (@Perp Tn A B C D)) *)
(* Goal: or (@Perp Tn A B C D) (not (@Perp Tn A B C D)) *)
      induction (perp_in_dec C A B C D).
(* Goal: or (@Bet Tn B P T) (@Bet Tn B T P) *)
(* Goal: or (@Bet Tn B P T) (@Bet Tn B T P) *)
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
        left.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
        apply l8_14_2_1a with C;auto.
(* Goal: or (@Bet Tn B P T) (@Bet Tn B T P) *)
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
      right.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
      intro.
(* Goal: False *)
      apply H0. clear H0.
(* Goal: @Perp_at Tn C A B C D *)
(* Goal: or (@Perp Tn A B C D) (not (@Perp Tn A B C D)) *)
      apply perp_in_right_comm.
(* Goal: @Perp_at Tn C A B D C *)
(* Goal: or (@Perp Tn A B C D) (not (@Perp Tn A B C D)) *)
      apply (l8_15_1 A B D C).
(* Goal: @Col Tn A B C *)
(* Goal: @Perp Tn A B D C *)
(* Goal: or (@Perp Tn A B C D) (not (@Perp Tn A B C D)) *)
        apply perp_distinct in H1.
(* Goal: and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) C D)) *)
        intuition.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      apply perp_right_comm;assumption.
(* Goal: or (@Perp Tn A B C D) (not (@Perp Tn A B C D)) *)
    elim (l8_18_existence A B C H); intros P HP.
(* Goal: @Perp Tn A C B P *)
    spliter.
(* Goal: or (@Perp Tn A B C D) (not (@Perp Tn A B C D)) *)
    induction (eq_dec_points C D).
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @Par Tn A B P Q) *)
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @Par Tn A B P Q) *)
      subst.
(* Goal: or (@Bet Tn B P T) (@Bet Tn B T P) *)
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
      right.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
      intro.
(* Goal: False *)
(* Goal: or (@Perp Tn A B C D) (not (@Perp Tn A B C D)) *)
      assert (A <> B /\ D <> D) by (apply perp_distinct;assumption).
(* Goal: and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) C D)) *)
      intuition.
(* Goal: or (@Perp Tn A B C D) (not (@Perp Tn A B C D)) *)
    induction (col_dec P C D).
(* Goal: or (@Bet Tn B P T) (@Bet Tn B T P) *)
(* Goal: or (@Bet Tn B P T) (@Bet Tn B T P) *)
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
      left.
(* Goal: @Perp Tn A B C D *)
(* Goal: or (@Perp Tn A B C D) (not (@Perp Tn A B C D)) *)
      assert (A <> B /\ C <> P) by (apply perp_distinct;assumption).
(* Goal: @Perp Tn A C B P *)
      spliter.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
      apply perp_col1 with P;Col.
(* Goal: or (@Bet Tn B P T) (@Bet Tn B T P) *)
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
    right.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
    intro.
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
    apply H3.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
    apply col_permutation_2, cop_perp2__col with A B; [Cop|apply perp_sym;assumption..].
Qed.

Lemma col_cop2_perp2__col : forall X1 X2 Y1 Y2 A B,
 Perp X1 X2 A B -> Perp Y1 Y2 A B -> Col X1 Y1 Y2 ->
 Coplanar A B X2 Y1 -> Coplanar A B X2 Y2 -> Col X2 Y1 Y2.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: @Coplanar Tn A B X2 Y2 *)
(* Goal: @Col Tn X2 Y1 Y2 *)
    induction(eq_dec_points X1 Y2).
      subst Y2.
      assert(Perp Y1 X1 A B).
        eapply perp_col.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
          intro.
(* Goal: False *)
(* Goal: @Col Tn D T C *)
(* Goal: @Col Tn D T B *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)) *)
(* Goal: @TS Tn A C B D *)
          treat_equalities.
          apply perp_distinct in H0.
(* Goal: and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) C D)) *)
          intuition.
(* Goal: False *)
          apply H0.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
        Col.
(* Goal: @Col Tn C B D *)
      apply col_permutation_1.
      apply cop_perp2__col with A B.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
        assumption.
(* Goal: False *)
        apply H.
(* Goal: @Perp Tn P Q P P' *)
(* Goal: not (@eq (@Tpoint Tn) Q P) *)
(* Goal: not (@eq (@Tpoint Tn) P P') *)
(* Goal: @Col Tn P P Q *)
      apply perp_left_comm.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      assumption.
    assert(Perp Y2 X1 A B).
      eapply perp_col.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
        auto.
(* Goal: @Perp Tn P Q P P' *)
(* Goal: not (@eq (@Tpoint Tn) Q P) *)
(* Goal: not (@eq (@Tpoint Tn) P P') *)
(* Goal: @Col Tn P P Q *)
        apply perp_left_comm.
(* Goal: False *)
        apply H0.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
      Col.
    assert(Perp X1 Y2 A B).
(* Goal: @Perp Tn P Q P P' *)
(* Goal: not (@eq (@Tpoint Tn) Q P) *)
(* Goal: not (@eq (@Tpoint Tn) P P') *)
(* Goal: @Col Tn P P Q *)
      eapply perp_left_comm.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      assumption.
(* Goal: @Coplanar Tn A B X2 Y1 *)
(* Goal: @Col Tn X2 Y1 Y2 *)
    induction(eq_dec_points X1 Y1).
      subst Y1.
(* Goal: @Col Tn T C D *)
(* Goal: False *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)) *)
(* Goal: @TS Tn A C B D *)
      apply col_permutation_2.
      apply cop_perp2__col with A B; Cop.
    assert(Perp X1 Y1 A B).
      eauto using perp_left_comm, perp_col with col.
    assert (Col X1 X2 Y1).
      apply cop_perp2__col with A B; Perp; Cop.
(* Goal: @Col Tn A B X *)
    ColR.
Qed.

Lemma col_perp2_ncol__col : forall X1 X2 Y1 Y2 A B,
 Perp X1 X2 A B -> Perp Y1 Y2 A B ->
 Col X1 Y1 Y2 -> ~ Col X1 A B ->
 Col X2 Y1 Y2.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: @Col Tn X2 Y1 Y2 *)
    assert (Coplanar A B X2 Y1).
(* Goal: @Coplanar Tn A B X2 Y1 *)
(* Goal: @Col Tn X2 Y1 Y2 *)
      induction (eq_dec_points X1 Y1).
(* Goal: @Coplanar Tn A B X2 Y2 *)
(* Goal: @Coplanar Tn A B X2 Y2 *)
(* Goal: @Col Tn X2 Y1 Y2 *)
        subst; Cop.
(* Goal: @Coplanar Tn A B X2 Y2 *)
(* Goal: @Col Tn X2 Y1 Y2 *)
      apply coplanar_trans_1 with X1; [Cop..|].
(* Goal: @Coplanar Tn X1 A B Y1 *)
(* Goal: @Col Tn X2 Y1 Y2 *)
      assert (Perp Y1 X1 A B) by (apply perp_col with Y2; Col); Cop.
(* Goal: @Col Tn X2 Y1 Y2 *)
    assert (Coplanar A B X2 Y2).
(* Goal: @Coplanar Tn A B X2 Y2 *)
(* Goal: @Col Tn X2 Y1 Y2 *)
      induction (eq_dec_points X1 Y2).
(* Goal: @Coplanar Tn A B X2 Y2 *)
(* Goal: @Coplanar Tn A B X2 Y2 *)
(* Goal: @Col Tn X2 Y1 Y2 *)
        subst; Cop.
(* Goal: @Coplanar Tn A B X2 Y2 *)
(* Goal: @Col Tn X2 Y1 Y2 *)
      apply coplanar_trans_1 with X1; [Cop..|].
(* Goal: @Coplanar Tn X1 A B Y2 *)
(* Goal: @Col Tn X2 Y1 Y2 *)
      assert (Perp Y2 X1 A B) by (apply perp_col with Y1; Perp; Col); Cop.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
    apply col_cop2_perp2__col with X1 A B; assumption.
Qed.

Lemma l12_9 : forall A1 A2 B1 B2 C1 C2,
 Coplanar C1 C2 A1 B1 -> Coplanar C1 C2 A1 B2 ->
 Coplanar C1 C2 A2 B1 -> Coplanar C1 C2 A2 B2 ->
 Perp A1 A2 C1 C2 -> Perp B1 B2 C1 C2 ->
 Par A1 A2 B1 B2.
Proof.
(* Goal: forall (A1 A2 B1 B2 C1 C2 : @Tpoint Tn) (_ : @Perp Tn A1 A2 C1 C2) (_ : @Perp Tn B1 B2 C1 C2), @Par Tn A1 A2 B1 B2 *)
    intros A1 A2 B1 B2 C1 C2.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: @Par Tn A B B C *)
    unfold Par.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Par_strict Tn A B C D), and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) A D)) (and (not (@eq (@Tpoint Tn) B C)) (and (not (@eq (@Tpoint Tn) B D)) (not (@eq (@Tpoint Tn) C D)))))) *)
    unfold Par_strict.
(* Goal: or (and (not (@eq (@Tpoint Tn) A1 A2)) (and (not (@eq (@Tpoint Tn) B1 B2)) (and (@Coplanar Tn A1 A2 B1 B2) (not (@ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A1 A2) (@Col Tn X B1 B2))))))) (and (not (@eq (@Tpoint Tn) A1 A2)) (and (not (@eq (@Tpoint Tn) B1 B2)) (and (@Col Tn A1 B1 B2) (@Col Tn A2 B1 B2)))) *)
    assert(A1 <> A2 /\ C1 <> C2) by (apply perp_distinct;assumption).
(* Goal: or (and (not (@eq (@Tpoint Tn) A1 A2)) (and (not (@eq (@Tpoint Tn) B1 B2)) (and (@Coplanar Tn A1 A2 B1 B2) (not (@ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A1 A2) (@Col Tn X B1 B2))))))) (and (not (@eq (@Tpoint Tn) A1 A2)) (and (not (@eq (@Tpoint Tn) B1 B2)) (and (@Col Tn A1 B1 B2) (@Col Tn A2 B1 B2)))) *)
    assert(B1 <> B2 /\ C1 <> C2) by (apply perp_distinct;assumption).
(* Goal: @Perp Tn A C B P *)
    spliter.
(* Goal: or (and (not (@eq (@Tpoint Tn) A1 A2)) (and (not (@eq (@Tpoint Tn) B1 B2)) (and (@Coplanar Tn A1 A2 B1 B2) (not (@ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A1 A2) (@Col Tn X B1 B2))))))) (and (not (@eq (@Tpoint Tn) A1 A2)) (and (not (@eq (@Tpoint Tn) B1 B2)) (and (@Col Tn A1 B1 B2) (@Col Tn A2 B1 B2)))) *)
    induction(col_dec A1 B1 B2).
(* Goal: or (@Bet Tn B P T) (@Bet Tn B T P) *)
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
      right.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
      repeat split; auto.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
      apply col_cop2_perp2__col with A1 C1 C2; auto.
    (***********************************)
(* Goal: or (@Bet Tn B P T) (@Bet Tn B T P) *)
(* Goal: or (@Bet Tn B P T) (@Bet Tn B T P) *)
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
    left.
(* Goal: and (not (@Col Tn B A C)) (and (not (@Col Tn D A C)) (@ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)))) *)
(* Goal: @TS Tn A C B D *)
    repeat split.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      assumption.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      assumption.
(* Goal: @Coplanar Tn A1 A2 B1 B2 *)
(* Goal: not (@ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A1 A2) (@Col Tn X B1 B2))) *)
      induction (perp_not_col2 C1 C2 A1 A2); Perp.
(* Goal: @Coplanar Tn A1 A2 B1 B2 *)
(* Goal: @Coplanar Tn A1 A2 B1 B2 *)
(* Goal: not (@ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A1 A2) (@Col Tn X B1 B2))) *)
        apply coplanar_pseudo_trans with C1 C2 A1; Cop.
(* Goal: @Coplanar Tn A1 A2 B1 B2 *)
(* Goal: not (@ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A1 A2) (@Col Tn X B1 B2))) *)
        apply coplanar_pseudo_trans with C1 C2 A2; Cop.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
    intro.
(* Goal: False *)
    ex_and H10 AB.
(* Goal: False *)
(* Goal: @Col Tn D T C *)
(* Goal: @Col Tn D T B *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)) *)
(* Goal: @TS Tn A C B D *)
    apply H9.
(* Goal: @Col Tn A1 B1 B2 *)
    induction(eq_dec_points AB A1).
(* Goal: @Col Tn A1 B1 B2 *)
(* Goal: @Col Tn A1 B1 B2 *)
      subst AB.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      assumption.
(* Goal: @Col Tn A1 B1 B2 *)
    assert(Perp A1 AB C1 C2) by (eauto using perp_col with col).
(* Goal: @Col Tn A1 B1 B2 *)
    apply col_cop2_perp2__col with AB C1 C2; Perp.
Qed.

(** We show here that from the axioms of neutral geometry we can deduce the existence of a parallel line. 
This is important because it shows that axioms of neutral geometry are inconsistent with those of elliptic geometry as 
elliptic geometry assumes that no parallel lines exist. *)
(** This corresponds to l12_10 in Tarski's book. *)

Lemma parallel_existence : forall A B P, A <> B ->
 exists C, exists D, C<>D /\ Par A B C D /\ Col P C D.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (not (@eq (@Tpoint Tn) C D)) (and (@Par Tn A B C D) (@Col Tn P C D)))) *)
    induction(col_dec A B P).
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A B) (@Col Tn X C D)) *)
(* Goal: @OS Tn B D A C *)
      exists A.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A B) (@Col Tn X C D)) *)
(* Goal: not (@TS Tn B D A C) *)
      exists B.
(* Goal: and (not (@Col Tn B A C)) (and (not (@Col Tn D A C)) (@ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)))) *)
(* Goal: @TS Tn A C B D *)
      repeat split.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
        assumption.
(* Goal: @Par Tn A B A B *)
(* Goal: @Col Tn P A B *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (not (@eq (@Tpoint Tn) C D)) (and (@Par Tn A B C D) (@Col Tn P C D)))) *)
        Par.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
      Col.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (not (@eq (@Tpoint Tn) C D)) (and (@Par Tn A B C D) (@Col Tn P C D)))) *)
    assert(exists P', Col A B P' /\ Perp A B P P').
(* Goal: @ex (@Tpoint Tn) (fun P' : @Tpoint Tn => and (@Col Tn A B P') (@Perp Tn A B P P')) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (not (@eq (@Tpoint Tn) C D)) (and (@Par Tn A B C D) (@Col Tn P C D)))) *)
      eapply l8_18_existence.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      assumption.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (not (@eq (@Tpoint Tn) C D)) (and (@Par Tn A B C D) (@Col Tn P C D)))) *)
    ex_and H1 P'.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (not (@eq (@Tpoint Tn) C D)) (and (@Par Tn A B C D) (@Col Tn P C D)))) *)
    assert(P <> P').
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
      intro.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (not (@eq (@Tpoint Tn) C D)) (and (@Par Tn A B C D) (@Col Tn P C D)))) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (not (@eq (@Tpoint Tn) C D)) (and (@Par Tn A B C D) (@Col Tn P C D)))) *)
      subst P'.
(* Goal: False *)
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
      contradiction.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (not (@eq (@Tpoint Tn) C D)) (and (@Par Tn A B C D) (@Col Tn P C D)))) *)
    induction(eq_dec_points P' A).
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (not (@eq (@Tpoint Tn) C D)) (and (@Par Tn A B C D) (@Col Tn P C D)))) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (not (@eq (@Tpoint Tn) C D)) (and (@Par Tn A B C D) (@Col Tn P C D)))) *)
      subst P'.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (not (@eq (@Tpoint Tn) C D)) (and (@Par Tn A B C D) (@Col Tn P C D)))) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (not (@eq (@Tpoint Tn) C D)) (and (@Par Tn A B C D) (@Col Tn P C D)))) *)
      assert(exists Q, Per Q P A /\ Cong Q P A B /\ OS A P Q B).
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Per Tn Q P P') (and (@Cong Tn Q P A B) (@OS Tn P' P Q A))) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (not (@eq (@Tpoint Tn) C D)) (and (@Par Tn A B C D) (@Col Tn P C D)))) *)
        eapply ex_per_cong.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
          auto.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
          assumption.
(* Goal: @Col Tn A P P *)
(* Goal: not (@Col Tn A P B) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (not (@eq (@Tpoint Tn) C D)) (and (@Par Tn A B C D) (@Col Tn P C D)))) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (not (@eq (@Tpoint Tn) C D)) (and (@Par Tn A B C D) (@Col Tn P C D)))) *)
          apply col_trivial_2.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
        intro.
(* Goal: False *)
        apply H0.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
        Col.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (not (@eq (@Tpoint Tn) C D)) (and (@Par Tn A B C D) (@Col Tn P C D)))) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (not (@eq (@Tpoint Tn) C D)) (and (@Par Tn A B C D) (@Col Tn P C D)))) *)
      ex_and H4 Q.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn A B P) (and (@Col Tn C D P) (@Perp_at Tn P A B C D))) *)
      exists P.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (not (@eq (@Tpoint Tn) P D)) (and (@Par Tn A B P D) (@Col Tn P P D))) *)
      exists Q.
(* Goal: and (not (@eq (@Tpoint Tn) P Q)) (and (@Par Tn A B P Q) (@Col Tn P P Q)) *)
      assert(P <> Q).
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
        intro.
(* Goal: False *)
(* Goal: @Col Tn D T C *)
(* Goal: @Col Tn D T B *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)) *)
(* Goal: @TS Tn A C B D *)
        treat_equalities.
(* Goal: and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) C D)) *)
        intuition.
(* Goal: and (not (@Col Tn B A C)) (and (not (@Col Tn D A C)) (@ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)))) *)
(* Goal: @TS Tn A C B D *)
      repeat split.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
        assumption.
(* Goal: @Par Tn A B P Q *)
(* Goal: @Col Tn P P Q *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (not (@eq (@Tpoint Tn) C D)) (and (@Par Tn A B C D) (@Col Tn P C D)))) *)
        apply l12_9 with P A; Cop.
(* Goal: @Perp Tn P Q P A *)
(* Goal: @Col Tn P P Q *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (not (@eq (@Tpoint Tn) C D)) (and (@Par Tn A B C D) (@Col Tn P C D)))) *)
        apply per_perp_in in H4.
(* Goal: @Perp Tn P Q P A *)
(* Goal: not (@eq (@Tpoint Tn) Q P) *)
(* Goal: not (@eq (@Tpoint Tn) P A) *)
(* Goal: @Col Tn P P Q *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (not (@eq (@Tpoint Tn) C D)) (and (@Par Tn A B C D) (@Col Tn P C D)))) *)
          apply perp_in_perp_bis in H4.
(* Goal: @Perp Tn P Q P A *)
(* Goal: not (@eq (@Tpoint Tn) Q P) *)
(* Goal: not (@eq (@Tpoint Tn) P A) *)
(* Goal: @Col Tn P P Q *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (not (@eq (@Tpoint Tn) C D)) (and (@Par Tn A B C D) (@Col Tn P C D)))) *)
          induction H4.
(* Goal: @Perp Tn P Q P A *)
(* Goal: @Perp Tn P Q P A *)
(* Goal: not (@eq (@Tpoint Tn) Q P) *)
(* Goal: not (@eq (@Tpoint Tn) P A) *)
(* Goal: @Col Tn P P Q *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (not (@eq (@Tpoint Tn) C D)) (and (@Par Tn A B C D) (@Col Tn P C D)))) *)
            apply perp_distinct in H4.
(* Goal: @Perp Tn A C B P *)
            spliter.
(* Goal: @Perp Tn P Q P P' *)
(* Goal: @Perp Tn P Q P P' *)
(* Goal: not (@eq (@Tpoint Tn) Q P) *)
(* Goal: not (@eq (@Tpoint Tn) P P') *)
(* Goal: @Col Tn P P Q *)
            absurde.
(* Goal: @Perp Tn P Q P P' *)
(* Goal: not (@eq (@Tpoint Tn) Q P) *)
(* Goal: not (@eq (@Tpoint Tn) P P') *)
(* Goal: @Col Tn P P Q *)
          apply perp_left_comm.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
          assumption.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
          auto.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
        assumption.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
      Col.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (not (@eq (@Tpoint Tn) C D)) (and (@Par Tn A B C D) (@Col Tn P C D)))) *)
    assert(exists Q, Per Q P P' /\ Cong Q P A B /\ OS P' P Q A).
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => and (@Per Tn Q P P') (and (@Cong Tn Q P A B) (@OS Tn P' P Q A))) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (not (@eq (@Tpoint Tn) C D)) (and (@Par Tn A B C D) (@Col Tn P C D)))) *)
      eapply ex_per_cong.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
        auto.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
        assumption.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
        Col.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
      intro.
(* Goal: False *)
      apply H0.
(* Goal: @Col Tn A B P *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (not (@eq (@Tpoint Tn) C D)) (and (@Par Tn A B C D) (@Col Tn P C D)))) *)
      eapply (col_transitivity_1 _ P').
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
        auto.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
        Col.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
      Col.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (not (@eq (@Tpoint Tn) C D)) (and (@Par Tn A B C D) (@Col Tn P C D)))) *)
    ex_and H5 Q.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn A B P) (and (@Col Tn C D P) (@Perp_at Tn P A B C D))) *)
    exists P.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (not (@eq (@Tpoint Tn) P D)) (and (@Par Tn A B P D) (@Col Tn P P D))) *)
    exists Q.
(* Goal: and (not (@eq (@Tpoint Tn) P Q)) (and (@Par Tn A B P Q) (@Col Tn P P Q)) *)
    assert(P <> Q).
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
      intro.
(* Goal: False *)
(* Goal: @Col Tn D T C *)
(* Goal: @Col Tn D T B *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)) *)
(* Goal: @TS Tn A C B D *)
      treat_equalities.
(* Goal: and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) C D)) *)
      intuition.
(* Goal: and (not (@Col Tn B A C)) (and (not (@Col Tn D A C)) (@ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)))) *)
(* Goal: @TS Tn A C B D *)
    repeat split.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      assumption.
(* Goal: @Par Tn A B P Q *)
(* Goal: @Col Tn P P Q *)
      apply l12_9 with P P'.
(* Goal: and (@Col Tn P A B) (@Col Tn P X Y) *)
(* Goal: False *)
        exists P; left; split; Col.
(* Goal: @Coplanar Tn P P' A Q *)
(* Goal: @Coplanar Tn P P' B P *)
(* Goal: @Coplanar Tn P P' B Q *)
(* Goal: @Perp Tn A B P P' *)
(* Goal: @Perp Tn P Q P P' *)
(* Goal: @Col Tn P P Q *)
        Cop.
(* Goal: and (@Col Tn P A B) (@Col Tn P X Y) *)
(* Goal: False *)
        exists P; left; split; Col.
(* Goal: @Coplanar Tn P P' A Q *)
(* Goal: @Coplanar Tn P P' B P *)
(* Goal: @Coplanar Tn P P' B Q *)
(* Goal: @Perp Tn A B P P' *)
(* Goal: @Perp Tn P Q P P' *)
(* Goal: @Col Tn P P Q *)
        apply coplanar_perm_3, col_cop__cop with A; Col; Cop.
(* Goal: @Perp Tn A B P P' *)
(* Goal: @Perp Tn P Q P P' *)
(* Goal: @Col Tn P P Q *)
        apply H2.
(* Goal: @Perp Tn P Q P P' *)
(* Goal: @Col Tn P P Q *)
      apply per_perp_in in H5.
(* Goal: @Perp Tn P Q P P' *)
(* Goal: not (@eq (@Tpoint Tn) Q P) *)
(* Goal: not (@eq (@Tpoint Tn) P P') *)
(* Goal: @Col Tn P P Q *)
        apply perp_in_perp_bis in H5.
(* Goal: or (@Bet Tn B P T) (@Bet Tn B T P) *)
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
        induction H5.
(* Goal: @Perp Tn P Q P P' *)
(* Goal: @Perp Tn P Q P P' *)
(* Goal: not (@eq (@Tpoint Tn) Q P) *)
(* Goal: not (@eq (@Tpoint Tn) P P') *)
(* Goal: @Col Tn P P Q *)
          apply perp_distinct in H5.
(* Goal: @Perp Tn A C B P *)
          spliter.
(* Goal: @Perp Tn P Q P P' *)
(* Goal: @Perp Tn P Q P P' *)
(* Goal: not (@eq (@Tpoint Tn) Q P) *)
(* Goal: not (@eq (@Tpoint Tn) P P') *)
(* Goal: @Col Tn P P Q *)
          absurde.
(* Goal: @Perp Tn P Q P P' *)
(* Goal: not (@eq (@Tpoint Tn) Q P) *)
(* Goal: not (@eq (@Tpoint Tn) P P') *)
(* Goal: @Col Tn P P Q *)
        apply perp_left_comm.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
        assumption.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
        auto.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      assumption.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
    Col.
Qed.

Lemma par_col_par : forall A B C D D',
 C <> D' -> Par A B C D -> Col C D D' -> Par A B C D'.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
    unfold Par in *.
    induction H0.
(* Goal: or (@Bet Tn B P T) (@Bet Tn B T P) *)
(* Goal: or (@Bet Tn B P T) (@Bet Tn B T P) *)
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
      left.
(* Goal: @Par_strict Tn B A C D *)
(* Goal: or (@Par_strict Tn B A C D) (and (not (@eq (@Tpoint Tn) B A)) (and (not (@eq (@Tpoint Tn) C D)) (and (@Col Tn B C D) (@Col Tn A C D)))) *)
      unfold Par_strict in *.
(* Goal: @Perp Tn A C B P *)
      spliter.
(* Goal: and (not (@Col Tn B A C)) (and (not (@Col Tn D A C)) (@ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)))) *)
(* Goal: @TS Tn A C B D *)
      repeat split.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
        assumption.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
        assumption.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
        apply col_cop__cop with D; auto.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
      intro.
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
      apply H4.
      ex_and H5 P.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn A B P) (and (@Col Tn C D P) (@Perp_at Tn P A B C D))) *)
      exists P.
(* Goal: and (@Col Tn C D P) (@Perp_at Tn P A B C D) *)
      split.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
        assumption.
(* Goal: @Col Tn T C D *)
(* Goal: False *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)) *)
(* Goal: @TS Tn A C B D *)
      apply col_permutation_2.
      eapply col_transitivity_1.
(* Goal: False *)
        apply H.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
        Col.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
      Col.
(* Goal: or (@Bet Tn B P T) (@Bet Tn B T P) *)
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
    right.
(* Goal: @Perp Tn A C B P *)
    spliter.
(* Goal: and (not (@Col Tn B A C)) (and (not (@Col Tn D A C)) (@ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)))) *)
(* Goal: @TS Tn A C B D *)
    repeat split.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      assumption.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      assumption.
(* Goal: @Col Tn T C D *)
(* Goal: False *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)) *)
(* Goal: @TS Tn A C B D *)
      apply col_permutation_2.
      eapply col_transitivity_1.
(* Goal: @Perp Tn A B P P' *)
(* Goal: @Perp Tn P Q P P' *)
(* Goal: @Col Tn P P Q *)
        apply H2.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
        assumption.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
      Col.
(* Goal: @Col Tn T C D *)
(* Goal: False *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)) *)
(* Goal: @TS Tn A C B D *)
    apply col_permutation_2.
    eapply col_transitivity_1.
(* Goal: @Perp Tn A B P P' *)
(* Goal: @Perp Tn P Q P P' *)
(* Goal: @Col Tn P P Q *)
      apply H2.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      assumption.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
    Col.
Qed.

Lemma parallel_existence1 : forall A B P, A <> B -> exists Q, Par A B P Q.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @Par Tn A B P Q) *)
    assert (T:= parallel_existence A B P H).
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @Par Tn A B P Q) *)
    decompose [and ex] T;clear T.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
    elim (eq_dec_points x P);intro.
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @Par Tn A B P Q) *)
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @Par Tn A B P Q) *)
      subst.
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @Par Tn A B P Q) *)
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @Par Tn A B P Q) *)
      exists x0.
(* Goal: and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) C D)) *)
      intuition.
(* Goal: @ex (@Tpoint Tn) (fun Q : @Tpoint Tn => @Par Tn A B P Q) *)
    exists x.
(* Goal: @Par Tn A B P x *)
    apply par_right_comm.
(* Goal: @Par Tn A B A B *)
(* Goal: @Col Tn P A B *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (not (@eq (@Tpoint Tn) C D)) (and (@Par Tn A B C D) (@Col Tn P C D)))) *)
    apply par_col_par with x0; Par.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
    Col.
Qed.

Lemma par_not_col : forall A B C D X, Par_strict A B C D -> Col X A B -> ~Col X C D.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: and (@OS Tn A C B D) (@OS Tn B D A C) *)
    unfold Par_strict in H.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
    intro.
(* Goal: @Perp Tn A C B P *)
    spliter.
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
    apply H4.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
    exists X; Col.
Qed.

Lemma not_strict_par1 : forall A B C D X, Par A B C D -> Col A B X -> Col C D X -> Col A B C.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: @TS Tn A C B D *)
    unfold Par in H.
(* Goal: @TS Tn A C B D *)
    induction H.
(* Goal: and (@OS Tn A C B D) (@OS Tn B D A C) *)
      unfold Par_strict in H.
(* Goal: @Perp Tn A C B P *)
      spliter.
      assert(exists X, Col X A B /\ Col X C D).
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A B) (@Col Tn X C D)) *)
(* Goal: @Bet Tn B T D *)
(* Goal: @TS Tn A C B D *)
        exists X.
(* Goal: and (@Col Tn P A B) (@Col Tn P X Y) *)
(* Goal: False *)
        split; Col.
(* Goal: False *)
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
      contradiction.
(* Goal: @Perp Tn A C B P *)
    spliter.
(* Goal: @Col Tn C B D *)
    apply col_permutation_1.
    eapply col_transitivity_1.
(* Goal: @Perp Tn A B P P' *)
(* Goal: @Perp Tn P Q P P' *)
(* Goal: @Col Tn P P Q *)
      apply H2.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
      Col.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
    Col.
Qed.

Lemma not_strict_par2 : forall A B C D X, Par A B C D -> Col A B X -> Col C D X -> Col A B D.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
    eapply not_strict_par1.
(* Goal: @Par Tn A B P x *)
      apply par_right_comm.
(* Goal: False *)
      apply H.
(* Goal: False *)
      apply H0.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
    Col.
Qed.

Lemma not_strict_par : forall A B C D X, Par A B C D -> Col A B X -> Col C D X -> Col A B C /\ Col A B D.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: and (@Col Tn C D P) (@Perp_at Tn P A B C D) *)
    split.
      eapply not_strict_par1.
(* Goal: False *)
        apply H.
(* Goal: False *)
        apply H0.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      assumption.
    eapply not_strict_par2.
(* Goal: False *)
      apply H.
(* Goal: False *)
      apply H0.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
    assumption.
Qed.

Lemma not_par_not_col : forall A B C, A <> B -> A <> C -> ~Par A B A C -> ~Col A B C.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
    intro.
(* Goal: @CongA Tn A B P C B P *)
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
    apply H1.
(* Goal: @Par Tn A B B C *)
    unfold Par.
(* Goal: or (@Bet Tn B P T) (@Bet Tn B T P) *)
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
    right.
(* Goal: and (not (@Col Tn B A C)) (and (not (@Col Tn D A C)) (@ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)))) *)
(* Goal: @TS Tn A C B D *)
    repeat split.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      assumption.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      assumption.
(* Goal: @Col Tn A A B *)
(* Goal: @Col Tn A C D *)
(* Goal: @Col Tn D T C *)
(* Goal: @Col Tn D T B *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)) *)
(* Goal: @TS Tn A C B D *)
      apply col_trivial_1.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
    Col.
Qed.

Lemma not_par_inter_uniqueness : forall A B C D X Y,
  A <> B -> C <> D -> ~Par A B C D -> Col A B X -> Col C D X -> Col A B Y -> Col C D Y ->
  X = Y.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
    induction(eq_dec_points C Y).
(* Goal: False *)
(* Goal: False *)
      subst Y.
      induction (eq_dec_points C X).
        subst X.
        reflexivity.
      eapply l6_21.
(* Goal: False *)
        2: apply H.
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
        2: apply H3.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
        intro.
(* Goal: @CongA Tn A B P C B P *)
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
        apply H1.
(* Goal: @Par Tn A B B C *)
        unfold Par.
(* Goal: or (@Bet Tn B P T) (@Bet Tn B T P) *)
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
        right.
(* Goal: @Col Tn A B X *)
        repeat split; assumption || ColR.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
        assumption.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
        assumption.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
        assumption.
    eapply l6_21.
(* Goal: False *)
      2: apply H0.
(* Goal: @Perp Tn A B P P' *)
(* Goal: @Perp Tn P Q P P' *)
(* Goal: @Col Tn P P Q *)
      2: apply H2.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
      intro.
(* Goal: @CongA Tn A B P C B P *)
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
      apply H1.
(* Goal: @Par Tn A B B C *)
      unfold Par.
(* Goal: or (@Bet Tn B P T) (@Bet Tn B T P) *)
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
      right.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      repeat split; ColR || assumption.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      assumption.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      assumption.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      assumption.
Qed.

Lemma inter_uniqueness_not_par : forall A B C D P,
  ~Col A B C -> Col A B P -> Col C D P -> ~Par A B C D.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
    intro.
(* Goal: False *)
    unfold Par in H2.
(* Goal: False *)
    induction H2.
(* Goal: False *)
(* Goal: False *)
      unfold Par_strict in H2.
(* Goal: @Perp Tn A C B P *)
      spliter.
(* Goal: False *)
(* Goal: False *)
      apply H5.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn A B P) (and (@Col Tn C D P) (@Perp_at Tn P A B C D))) *)
      exists P.
(* Goal: and (@Col Tn P A B) (@Col Tn P C D) *)
(* Goal: False *)
      Col5.
(* Goal: @Perp Tn A C B P *)
    spliter.
(* Goal: False *)
    apply H.
(* Goal: @Col Tn A B X *)
    ColR.
Qed.

Lemma col_not_col_not_par :
 forall A B C D,
 (exists P, Col A B P /\ Col C D P) ->
 (exists Q, Col C D Q /\ ~Col A B Q) -> ~Par A B C D.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
    ex_and H P.
    ex_and H0 Q.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
    intro.
    unfold Par in H3.
    induction H3.
      unfold Par_strict in H3.
(* Goal: @Perp Tn A C B P *)
      spliter.
      apply H6.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn A B P) (and (@Col Tn C D P) (@Perp_at Tn P A B C D))) *)
      exists P.
(* Goal: and (@Col Tn P A B) (@Col Tn P C D) *)
(* Goal: False *)
      Col5.
(* Goal: @Perp Tn A C B P *)
    spliter.
(* Goal: @Perp Tn A B P P' *)
(* Goal: @Perp Tn P Q P P' *)
(* Goal: @Col Tn P P Q *)
    apply H2.
    eapply col3.
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
      apply H4.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
      Col.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
      Col.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
    Col.
Qed.

Lemma par_distincts : forall A B C D,
 Par A B C D -> (Par A B C D /\ A <> B /\ C <> D).
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: and (@Col Tn C D P) (@Perp_at Tn P A B C D) *)
    split.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      assumption.
(* Goal: @TS Tn A C B D *)
    unfold Par in H.
(* Goal: @TS Tn A C B D *)
    induction H.
(* Goal: and (@OS Tn A C B D) (@OS Tn B D A C) *)
      unfold Par_strict in H.
(* Goal: @Perp Tn A C B P *)
      spliter.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      split; assumption.
(* Goal: @Perp Tn A C B P *)
    spliter.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
    split; assumption.
Qed.

Lemma par_not_col_strict : forall A B C D P,
 Par A B C D -> Col C D P -> ~Col A B P -> Par_strict A B C D.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: @Par Tn A B D C *)
    apply par_symmetry in H.
(* Goal: @TS Tn A C B D *)
    unfold Par in H.
(* Goal: @TS Tn A C B D *)
    induction H.
(* Goal: @Par_strict Tn C D A B *)
      apply par_strict_symmetry.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      assumption.
(* Goal: @Perp Tn A C B P *)
    spliter.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Par_strict Tn A B C D), and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) A D)) (and (not (@eq (@Tpoint Tn) B C)) (and (not (@eq (@Tpoint Tn) B D)) (not (@eq (@Tpoint Tn) C D)))))) *)
    unfold Par_strict.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
    repeat split; auto.
(* Goal: and (@Col Tn P A B) (@Col Tn P X Y) *)
(* Goal: False *)
      exists C; left; split; Col.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
    intro.
    ex_and H5 X.
(* Goal: @CongA Tn A B P C B P *)
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
    apply H1.
    assert(Col A C D).
      eapply (col_transitivity_1 _ B).
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
        assumption.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
        Col.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
      Col.
    assert(Col B C D).
(* Goal: @Col Tn C T B *)
(* Goal: False *)
(* Goal: not (@Col Tn D A C) *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)) *)
(* Goal: @TS Tn A C B D *)
      eapply (col_transitivity_1 _ A).
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
        auto.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
        Col.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
      Col.
    eapply col3.
(* Goal: False *)
      apply H.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
      Col.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
      Col.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
    Col.
Qed.

Lemma all_one_side_par_strict : forall A B C D,
 C <> D -> (forall P, Col C D P -> OS A B C P) ->
 Par_strict A B C D.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Par_strict Tn A B C D), and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) A D)) (and (not (@eq (@Tpoint Tn) B C)) (and (not (@eq (@Tpoint Tn) B D)) (not (@eq (@Tpoint Tn) C D)))))) *)
    unfold Par_strict.
(* Goal: and (not (@Col Tn B A C)) (and (not (@Col Tn D A C)) (@ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)))) *)
(* Goal: @TS Tn A C B D *)
    repeat split.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: not (@eq (@Tpoint Tn) C D) *)
(* Goal: @Coplanar Tn A B C D *)
(* Goal: not (@ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A B) (@Col Tn X C D))) *)
      assert(HH:=H0 D (col_trivial_2 _ _)).
(* Goal: False *)
      unfold OS in HH.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: not (@eq (@Tpoint Tn) C D) *)
(* Goal: @Coplanar Tn A B C D *)
(* Goal: not (@ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A B) (@Col Tn X C D))) *)
      ex_and HH C0.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: not (@eq (@Tpoint Tn) C D) *)
(* Goal: @Coplanar Tn A B C D *)
(* Goal: not (@ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A B) (@Col Tn X C D))) *)
      unfold TS in H1.
(* Goal: @Perp Tn A C B P *)
      spliter.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
        intro.
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
        subst B.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
        Col.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      assumption.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
      apply os__coplanar, H0; Col.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
    intro.
(* Goal: False *)
    ex_and H1 X.
(* Goal: False *)
    assert(HH:= H0 X (col_permutation_1 _ _ _ H2) ).
(* Goal: False *)
    unfold OS in HH.
(* Goal: False *)
    ex_and HH M.
(* Goal: False *)
    unfold TS in H4.
(* Goal: @Perp Tn A C B P *)
    spliter.
(* Goal: False *)
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
    contradiction.
Qed.

Lemma par_col_par_2 : forall A B C D P,
 A <> P -> Col A B P -> Par A B C D -> Par A P C D.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
    unfold Par in *.
(* Goal: False *)
    induction H1.
(* Goal: or (@Bet Tn B P T) (@Bet Tn B T P) *)
(* Goal: or (@Bet Tn B P T) (@Bet Tn B T P) *)
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
      left.
(* Goal: @Par_strict Tn B A C D *)
(* Goal: or (@Par_strict Tn B A C D) (and (not (@eq (@Tpoint Tn) B A)) (and (not (@eq (@Tpoint Tn) C D)) (and (@Col Tn B C D) (@Col Tn A C D)))) *)
      unfold Par_strict in *.
(* Goal: @Perp Tn A C B P *)
      spliter.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
      repeat split; auto.
(* Goal: @Coplanar Tn P P' A Q *)
(* Goal: @Coplanar Tn P P' B P *)
(* Goal: @Coplanar Tn P P' B Q *)
(* Goal: @Perp Tn A B P P' *)
(* Goal: @Perp Tn P Q P P' *)
(* Goal: @Col Tn P P Q *)
      apply coplanar_perm_16, col_cop__cop with B; Cop.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
      intro.
      ex_and H5 X.
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
      apply H4.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A B) (@Col Tn X C D)) *)
(* Goal: @Bet Tn B T D *)
(* Goal: @TS Tn A C B D *)
      exists X.
(* Goal: and (@Col Tn C D P) (@Perp_at Tn P A B C D) *)
      split.
(* Goal: @Col Tn A B X *)
        ColR.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
      Col.
(* Goal: or (@Bet Tn B P T) (@Bet Tn B T P) *)
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
    right.
(* Goal: @Perp Tn A C B P *)
    spliter.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
    repeat split;auto.
    assert(Col A B D).
(* Goal: @Col Tn A B X *)
      ColR.
    assert(Col A B C).
(* Goal: @Col Tn A B X *)
      ColR.
    eapply col3.
(* Goal: @CongA Tn A B P C B P *)
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
      apply H1.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
      Col.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
      Col.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
    Col.
Qed.


Lemma par_col2_par : forall A B C D E F,
 E <> F -> Par A B C D -> Col C D E -> Col C D F -> Par A B E F.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
    induction (eq_dec_points C E).
      subst E.
      eapply par_col_par.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
        assumption.
(* Goal: False *)
        apply H0.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      assumption.
    eapply par_col_par.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      assumption.
(* Goal: @Par Tn A B P x *)
      apply par_right_comm.
      eapply par_col_par.
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
        apply H3.
(* Goal: False *)
        apply H0.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      assumption.
(* Goal: @Col Tn T C D *)
(* Goal: False *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)) *)
(* Goal: @TS Tn A C B D *)
    apply col_permutation_2.
    eapply col_transitivity_1.
      apply par_distincts in H0.
(* Goal: @Perp Tn A C B P *)
      spliter.
(* Goal: False *)
(* Goal: False *)
      apply H5.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      assumption.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
    assumption.
Qed.

Lemma par_col2_par_bis : forall A B C D E F,
 E <> F -> Par A B C D -> Col E F C -> Col E F D -> Par A B E F.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
intros.
(* Goal: @Col Tn A B X *)
apply par_col2_par with C D; Col; ColR.
Qed.

Lemma par_strict_col_par_strict : forall A B C D E,
 C <> E -> Par_strict A B C D -> Col C D E ->
 Par_strict A B C E.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
    assert(Par C E A B).
      eapply par_col_par_2.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
        auto.
(* Goal: @CongA Tn A B P C B P *)
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
        apply H1.
(* Goal: @Par Tn E F C D *)
      apply par_symmetry.
(* Goal: or (@Bet Tn B P T) (@Bet Tn B T P) *)
(* Goal: or (@Bet Tn B P T) (@Bet Tn B T P) *)
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
      left.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      assumption.
(* Goal: False *)
    induction H2.
(* Goal: @Par_strict Tn C D A B *)
      apply par_strict_symmetry.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      assumption.
    unfold Par_strict in H0.
(* Goal: @Perp Tn A C B P *)
    spliter.
(* Goal: @TS Tn A C B D *)
    apply False_ind.
    apply H8.
(* Goal: @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => and (@Midpoint Tn T A C') (@Cong Tn B A B C')) *)
(* Goal: @Perp Tn A C B P *)
    exists C.
(* Goal: and (@Col Tn P A B) (@Col Tn P X Y) *)
(* Goal: False *)
    split; Col.
Qed.

Lemma par_strict_col2_par_strict : forall A B C D E F,
 E <> F -> Par_strict A B C D -> Col C D E -> Col C D F ->
 Par_strict A B E F.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: @Par_strict Tn B A C D *)
(* Goal: or (@Par_strict Tn B A C D) (and (not (@eq (@Tpoint Tn) B A)) (and (not (@eq (@Tpoint Tn) C D)) (and (@Col Tn B C D) (@Col Tn A C D)))) *)
    unfold Par_strict in *.
(* Goal: @Perp Tn A C B P *)
    spliter.
(* Goal: and (not (@Col Tn B A C)) (and (not (@Col Tn D A C)) (@ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)))) *)
(* Goal: @TS Tn A C B D *)
    repeat split.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      assumption.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      assumption.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      apply col2_cop__cop with C D; assumption.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
    intro.
(* Goal: False *)
(* Goal: False *)
    apply H5.
    ex_and H6 X.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A B) (@Col Tn X C D)) *)
(* Goal: @Bet Tn B T D *)
(* Goal: @TS Tn A C B D *)
    exists X.
(* Goal: and (@Col Tn C D P) (@Perp_at Tn P A B C D) *)
    split.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      assumption.
    assert(Col C E F).
      eapply col_transitivity_1.
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
        apply H3.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
        assumption.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      assumption.
    assert(Col D E F).
(* Goal: @Col Tn D C B *)
      eapply (col_transitivity_1 _ C).
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
        auto.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
        Col.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
      Col.
    eapply col3.
(* Goal: False *)
      apply H.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
      Col.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
      Col.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
    Col.
Qed.

Lemma line_dec : forall B1 B2 C1 C2, (Col C1 B1 B2 /\ Col C2 B1 B2) \/ ~ (Col C1 B1 B2 /\ Col C2 B1 B2).
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
    induction (col_dec C1 B1 B2); induction (col_dec C2 B1 B2);tauto.
Qed.

Lemma par_distinct : forall A B C D, Par A B C D -> A <> B /\ C <> D.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: @TS Tn A C B D *)
    induction H.
(* Goal: and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) C D)) *)
      unfold Par_strict in H; intuition.
(* Goal: and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) C D)) *)
    intuition.
Qed.

Lemma par_col4__par : forall A B C D E F G H, E <> F -> G <> H -> Par A B C D ->
 Col A B E -> Col A B F -> Col C D G -> Col C D H -> Par E F G H.
Proof.
(* Goal: forall (A B C D E F G H : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) E F)) (_ : not (@eq (@Tpoint Tn) G H)) (_ : @Par Tn A B C D) (_ : @Col Tn A B E) (_ : @Col Tn A B F) (_ : @Col Tn C D G) (_ : @Col Tn C D H), @Par Tn E F G H *)
    intros A B C D E F G H.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
    apply (par_col2_par _ _ C D); auto.
(* Goal: @Par Tn E F C D *)
    apply par_symmetry.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
    apply (par_col2_par _ _ A B); auto.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
    apply par_symmetry; auto.
Qed.

Lemma par_strict_col4__par_strict : forall A B C D E F G H, E <> F -> G <> H ->
 Par_strict A B C D -> Col A B E -> Col A B F -> Col C D G -> Col C D H ->
 Par_strict E F G H.
Proof.
(* Goal: forall (A B C D E F G H : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) E F)) (_ : not (@eq (@Tpoint Tn) G H)) (_ : @Par Tn A B C D) (_ : @Col Tn A B E) (_ : @Col Tn A B F) (_ : @Col Tn C D G) (_ : @Col Tn C D H), @Par Tn E F G H *)
    intros A B C D E F G H.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
    apply (par_strict_col2_par_strict _ _ C D); auto.
(* Goal: @Par_strict Tn C D A B *)
    apply par_strict_symmetry.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
    apply (par_strict_col2_par_strict _ _ A B); auto.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
    apply par_strict_symmetry; auto.
Qed.

Lemma par_strict_one_side : forall A B C D P,
 Par_strict A B C D -> Col C D P -> OS A B C P.
Proof.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
  intros A B C D P HPar HCol.
(* Goal: @OS Tn A B C P *)
  destruct (eq_dec_points C P).
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
    subst P; apply par_strict_not_col_1 in HPar; apply one_side_reflexivity; Col.
(* Goal: @OS Tn A B C P *)
  apply l12_6, par_strict_col_par_strict with D; trivial.
Qed.

Lemma par_strict_all_one_side : forall A B C D,
 Par_strict A B C D -> (forall P, Col C D P -> OS A B C P).
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
    eapply par_strict_one_side.
(* Goal: False *)
      apply H.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
    assumption.
Qed.

Lemma inter_distincts : forall A B C D X, Inter A B C D X -> A <> B /\ C <> D.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) C D)) *)
    destruct H as [HAB [[P []] _]].
(* Goal: @InAngle Tn P A B C *)
    assert_diffs.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
    split; auto.
Qed.

Lemma inter_trivial : forall A B X, ~ Col A B X -> Inter A X B X X.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: @InAngle Tn P A B C *)
    assert_diffs.
(* Goal: @Inter Tn A X B X X *)
    unfold Inter.
(* Goal: and (@Col Tn P A B) (@Col Tn P X Y) *)
(* Goal: False *)
    repeat split; Col.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A B) (@Col Tn X C D)) *)
(* Goal: not (@TS Tn B D A C) *)
      exists B.
(* Goal: and (@Col Tn C D P) (@Perp_at Tn P A B C D) *)
      split.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
        Col.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
      intro.
(* Goal: False *)
      apply H.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
      Col.
Qed.

Lemma inter_sym : forall A B C D X, Inter A B C D X -> Inter C D A B X.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: @Inter Tn A B D C X *)
    unfold Inter in *.
(* Goal: @Perp Tn A C B P *)
    spliter.
(* Goal: and (not (@eq (@Tpoint Tn) D C)) (and (@ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn P D C) (not (@Col Tn P A B)))) (and (@Col Tn A B X) (@Col Tn D C X))) *)
    ex_and H0 P.
(* Goal: @Perp Tn A C B P *)
    assert(A <> B).
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
      intro.
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
      subst B.
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
      apply H3.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
      Col.
(* Goal: and (@Col Tn C D P) (@Perp_at Tn P A B C D) *)
    split.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      assumption.
(* Goal: and (@Col Tn C D P) (@Perp_at Tn P A B C D) *)
    split.
      induction(eq_dec_points A X).
(* Goal: False *)
(* Goal: @Col Tn D T C *)
(* Goal: @Col Tn D T B *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)) *)
(* Goal: @TS Tn A C B D *)
        treat_equalities.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A B) (@Col Tn X C D)) *)
(* Goal: not (@TS Tn B D A C) *)
        exists B.
(* Goal: and (@Col Tn C D P) (@Perp_at Tn P A B C D) *)
        split.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
          Col.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
        intro.
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
        apply H3.
        eapply col3.
(* Goal: False *)
          apply H.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
          Col.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
          Col.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
        Col.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A B) (@Col Tn X C D)) *)
(* Goal: @OS Tn B D A C *)
      exists A.
(* Goal: and (@Col Tn C D P) (@Perp_at Tn P A B C D) *)
      split.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
        Col.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
      intro.
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
      apply H3.
      assert(Col A P X).
        eapply col3.
(* Goal: False *)
          apply H.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
          Col.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
          Col.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
        Col.
(* Goal: @Col Tn A B X *)
      ColR.
(* Goal: and (@Col Tn P A B) (@Col Tn P X Y) *)
(* Goal: False *)
    split; Col.
Qed.

Lemma inter_left_comm : forall A B C D X, Inter A B C D X -> Inter B A C D X.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: @Inter Tn A B D C X *)
    unfold Inter in *.
(* Goal: @Perp Tn A C B P *)
    spliter.
(* Goal: and (not (@eq (@Tpoint Tn) D C)) (and (@ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn P D C) (not (@Col Tn P A B)))) (and (@Col Tn A B X) (@Col Tn D C X))) *)
    ex_and H0 P.
(* Goal: and (@Col Tn C D P) (@Perp_at Tn P A B C D) *)
    split.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      assumption.
(* Goal: and (@Col Tn C D P) (@Perp_at Tn P A B C D) *)
    split.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn A B P) (and (@Col Tn C D P) (@Perp_at Tn P A B C D))) *)
      exists P.
(* Goal: and (@Col Tn C D P) (@Perp_at Tn P A B C D) *)
      split.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
        assumption.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
      intro.
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
      apply H3.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
      Col.
(* Goal: and (@Col Tn P A B) (@Col Tn P X Y) *)
(* Goal: False *)
    split; Col.
Qed.

Lemma inter_right_comm : forall A B C D X, Inter A B C D X -> Inter A B D C X.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: @Inter Tn A B D C X *)
    unfold Inter in *.
(* Goal: @Perp Tn A C B P *)
    spliter.
(* Goal: and (not (@eq (@Tpoint Tn) D C)) (and (@ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn P D C) (not (@Col Tn P A B)))) (and (@Col Tn A B X) (@Col Tn D C X))) *)
    ex_and H0 P.
(* Goal: and (@Col Tn C D P) (@Perp_at Tn P A B C D) *)
    split.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
      auto.
(* Goal: and (@Col Tn C D P) (@Perp_at Tn P A B C D) *)
    split.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn A B P) (and (@Col Tn C D P) (@Perp_at Tn P A B C D))) *)
      exists P.
(* Goal: and (@Col Tn C D P) (@Perp_at Tn P A B C D) *)
      split.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
        Col.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      assumption.
(* Goal: and (@Col Tn P A B) (@Col Tn P X Y) *)
(* Goal: False *)
    split; Col.
Qed.

Lemma inter_comm : forall A B C D X, Inter A B C D X -> Inter B A D C X.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: @Inter Tn B A D C X *)
    apply inter_left_comm.
(* Goal: @Inter Tn A B D C X *)
    apply inter_right_comm.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
    assumption.
Qed.

(** In the proof given by Tarski on page 125 the distinction of cases is explicit.
This is a good example on the significance of decidability. *)
Lemma l12_17 : forall A B C D P,
 A <> B -> Midpoint P A C -> Midpoint P B D -> Par A B C D.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (not (@eq (@Tpoint Tn) C D)) (and (@Par Tn A B C D) (@Col Tn P C D)))) *)
    induction(col_dec A B P).
(* Goal: @Par Tn A B B C *)
      unfold Par.
(* Goal: or (@Bet Tn B P T) (@Bet Tn B T P) *)
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
      right.
      induction(eq_dec_points A P).
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
        subst P.
        apply is_midpoint_id in H0.
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
        subst C.
(* Goal: and (not (@Col Tn B A C)) (and (not (@Col Tn D A C)) (@ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)))) *)
(* Goal: @TS Tn A C B D *)
        repeat split.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
          assumption.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
          intro.
(* Goal: False *)
(* Goal: @Col Tn D T C *)
(* Goal: @Col Tn D T B *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)) *)
(* Goal: @TS Tn A C B D *)
          treat_equalities.
          apply l7_2 in H1.
          apply is_midpoint_id in H1.
(* Goal: False *)
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
          contradiction.
(* Goal: @Col Tn A A B *)
(* Goal: @Col Tn A C D *)
(* Goal: @Col Tn D T C *)
(* Goal: @Col Tn D T B *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)) *)
(* Goal: @TS Tn A C B D *)
          apply col_trivial_1.
        unfold Midpoint in H1.
(* Goal: @Perp Tn A C B P *)
        spliter.
        apply bet_col.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
        assumption.
      induction(eq_dec_points B P).
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
        subst P.
        apply is_midpoint_id in H1.
(* Goal: False *)
(* Goal: and (@OS Tn A C B D) (@OS Tn B D A C) *)
        subst D.
(* Goal: and (not (@Col Tn B A C)) (and (not (@Col Tn D A C)) (@ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)))) *)
(* Goal: @TS Tn A C B D *)
        repeat split.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
          assumption.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
          intro.
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
          subst C.
          apply l7_2 in H0.
          apply is_midpoint_id in H0.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
          auto.
          unfold Midpoint in H0.
(* Goal: @Perp Tn A C B P *)
          spliter.
          apply bet_col in H0 .
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
          Col.
(* Goal: @Col Tn B A B *)
        apply col_trivial_3.
      assert(HH0 := H0).
      assert(HH1:= H1).
      unfold Midpoint in H0.
      unfold Midpoint in H1.
(* Goal: @Perp Tn A C B P *)
      spliter.
      apply bet_col in H1.
      apply bet_col in H0.
      assert(Col B C P).
(* Goal: @Col Tn C B D *)
        eapply col_permutation_1.
(* Goal: @Col Tn C T B *)
(* Goal: False *)
(* Goal: not (@Col Tn D A C) *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)) *)
(* Goal: @TS Tn A C B D *)
        eapply (col_transitivity_1 _ A).
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
          auto.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
          Col.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
        Col.
      assert(Col B C D).
        eapply (col_transitivity_1 _ P).
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
          assumption.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
          Col.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
        Col.
(* Goal: and (not (@Col Tn B A C)) (and (not (@Col Tn D A C)) (@ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)))) *)
(* Goal: @TS Tn A C B D *)
      repeat split.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
        assumption.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
        intro.
(* Goal: False *)
(* Goal: @Col Tn D T C *)
(* Goal: @Col Tn D T B *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)) *)
(* Goal: @TS Tn A C B D *)
        treat_equalities.
(* Goal: and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) C D)) *)
        intuition.
        induction(eq_dec_points A D).
(* Goal: False *)
(* Goal: and (@OS Tn A C B D) (@OS Tn B D A C) *)
          subst D.
(* Goal: @Col Tn B A B *)
          apply col_trivial_3.
        assert(Col C D P).
          eapply (col_transitivity_1 _ B).
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
            intro.
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
            subst C.
            assert(A = D).
              eapply symmetric_point_uniqueness.
                eapply l7_2.
                apply HH0.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
              assumption.
(* Goal: False *)
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
            contradiction.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
            Col.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
          Col.
        induction(eq_dec_points C P).
(* Goal: False *)
(* Goal: @Col Tn D T C *)
(* Goal: @Col Tn D T B *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)) *)
(* Goal: @TS Tn A C B D *)
          treat_equalities.
(* Goal: and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) C D)) *)
          intuition.
(* Goal: @Col Tn T C D *)
(* Goal: False *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)) *)
(* Goal: @TS Tn A C B D *)
        apply col_permutation_2.
        eapply (col_transitivity_1 _ P).
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
          assumption.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
          Col.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
        Col.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      assumption.
    (* cas non degenere *)
    assert(exists E, Col A B E /\ Perp A B P E).
(* Goal: @ex (@Tpoint Tn) (fun P' : @Tpoint Tn => and (@Col Tn A B P') (@Perp Tn A B P P')) *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (not (@eq (@Tpoint Tn) C D)) (and (@Par Tn A B C D) (@Col Tn P C D)))) *)
      eapply l8_18_existence.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      assumption.
    ex_and H3 E.
    assert(A <> P).
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
      intro.
(* Goal: False *)
(* Goal: @Col Tn D T C *)
(* Goal: @Col Tn D T B *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)) *)
(* Goal: @TS Tn A C B D *)
      treat_equalities.
(* Goal: @Perp Tn A B P P' *)
(* Goal: @Perp Tn P Q P P' *)
(* Goal: @Col Tn P P Q *)
      apply H2.
(* Goal: @Col Tn B A B *)
      apply col_trivial_3.
    induction(eq_dec_points A E).
(* Goal: False *)
(* Goal: @Col Tn D T C *)
(* Goal: @Col Tn D T B *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)) *)
(* Goal: @TS Tn A C B D *)
      treat_equalities.
      assert(Per P A B).
        eapply perp_in_per.
        apply perp_in_comm.
        eapply perp_perp_in.
(* Goal: @Perp Tn A C B P *)
(* Goal: not (@eq (@Tpoint Tn) T A) *)
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
        apply perp_sym.
        apply perp_comm.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
        assumption.
      prolong B A B' B A.
      prolong B' P D' B' P.
      assert(Midpoint C D D').
        eapply symmetry_preserves_midpoint.
(* Goal: @CongA Tn A B P C B P *)
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
          apply H1.
(* Goal: False *)
          apply H0.
(* Goal: and (@Col Tn C D P) (@Perp_at Tn P A B C D) *)
          split.
            apply H8.
          Cong.
(* Goal: and (@Col Tn C D P) (@Perp_at Tn P A B C D) *)
        split.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
          assumption.
        Cong.
      assert(Per P A B').
        eapply per_col.
(* Goal: False *)
          apply H.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
          assumption.
(* Goal: @Col Tn T A C *)
        apply bet_col in H6.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
        Col.
      ex_and H3 B''.
      assert(B' = B'').
        eapply symmetric_point_uniqueness.
(* Goal: and (@Col Tn C D P) (@Perp_at Tn P A B C D) *)
          split.
            apply H6.
          Cong.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
        assumption.
      subst B''.
      assert(Cong P D P D').
        apply  (cong_transitivity _ _ B P).
          unfold Midpoint in H1.
(* Goal: @Perp Tn A C B P *)
          spliter.
          Cong.
        apply  (cong_transitivity _ _ B' P).
          Cong.
        Cong.
      assert(Per P C D).
(* Goal: @Per Tn B T A *)
(* Goal: @Perp Tn A C B P *)
        unfold Per.
        exists D'.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
        split; assumption.
      apply per_perp_in in H14.
        apply perp_in_perp_bis in H14.
        induction H14.
          apply perp_distinct in H14.
(* Goal: and (not (@eq (@Tpoint Tn) A B)) (not (@eq (@Tpoint Tn) C D)) *)
          intuition.
(* Goal: @Par Tn A B P Q *)
(* Goal: @Col Tn P P Q *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (not (@eq (@Tpoint Tn) C D)) (and (@Par Tn A B C D) (@Col Tn P C D)))) *)
        eapply l12_9 with P A; Cop.
(* Goal: @Perp Tn A C B P *)
(* Goal: not (@eq (@Tpoint Tn) T A) *)
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
        apply perp_sym.
        eapply perp_col.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
          auto.
          apply H14.
        unfold Midpoint in H0.
(* Goal: @Perp Tn A C B P *)
        spliter.
        apply bet_col in H0.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
        Col.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
        intro.
(* Goal: False *)
(* Goal: @Col Tn D T C *)
(* Goal: @Col Tn D T B *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)) *)
(* Goal: @TS Tn A C B D *)
        treat_equalities.
        apply l7_2 in H0.
        eapply is_midpoint_id in H0.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
        auto.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
      intro.
(* Goal: False *)
(* Goal: and (@OS Tn A C B D) (@OS Tn B D A C) *)
      subst D.
      assert(C = D').
        apply is_midpoint_id.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
        assumption.
      subst D'.
      assert(A = B).
        eapply symmetric_point_uniqueness.
          apply l7_2.
(* Goal: False *)
          apply H0.
        apply l7_2.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
        assumption.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
      auto.
    prolong E P F E P.
    assert(Col C D F).
      eapply mid_preserves_col.
(* Goal: False *)
        2: apply H0.
(* Goal: @CongA Tn A B P C B P *)
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
        2:apply H1.
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
        apply H3.
(* Goal: and (@Col Tn C D P) (@Perp_at Tn P A B C D) *)
      split.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
        assumption.
      Cong.
    prolong A E A' A E.
    prolong A' P C' A' P.
    assert(Midpoint F C C').
      eapply symmetry_preserves_midpoint.
(* Goal: False *)
        apply H0.
(* Goal: and (@Col Tn C D P) (@Perp_at Tn P A B C D) *)
        split.
          apply H7.
        Cong.
(* Goal: and (@Col Tn C D P) (@Perp_at Tn P A B C D) *)
        split.
(* Goal: False *)
(* Goal: @Bet Tn B T D *)
(* Goal: @TS Tn A C B D *)
          apply H12.
        Cong.
(* Goal: and (@Col Tn C D P) (@Perp_at Tn P A B C D) *)
      split.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
        assumption.
      Cong.
    assert(Per P E A).
      eapply perp_in_per.
      apply perp_in_comm.
      apply perp_perp_in.
(* Goal: @Perp Tn A C B P *)
(* Goal: not (@eq (@Tpoint Tn) T A) *)
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
      apply perp_sym.
      eapply perp_col.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
        assumption.
(* Goal: @Perp Tn A C B P *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
        apply perp_right_comm.
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
        apply H4.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
      Col.
    assert(Cong P C P C').
      eapply (cong_transitivity _ _ P A).
        unfold Midpoint in H0.
(* Goal: @Perp Tn A C B P *)
        spliter.
        Cong.
      eapply (cong_transitivity _ _ P A').
        unfold Per in H15.
        ex_and H15 A''.
        assert( A' = A'').
          eapply symmetric_point_uniqueness.
(* Goal: and (@Col Tn C D P) (@Perp_at Tn P A B C D) *)
            split.
(* Goal: False *)
(* Goal: @Col Tn T A C *)
              apply H10.
            Cong.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
          assumption.
        subst A''.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
        assumption.
      Cong.
    assert(Per P F C).
(* Goal: @Per Tn B T A *)
(* Goal: @Perp Tn A C B P *)
      unfold Per.
      exists C'.
(* Goal: and (@Col Tn C D P) (@Perp_at Tn P A B C D) *)
      split.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
        assumption.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      assumption.
    apply per_perp_in in H17.
      apply perp_in_comm in H17.
      apply perp_in_perp_bis in H17.
      induction H17.
        apply l12_9 with P E.
(* Goal: and (@Col Tn P A B) (@Col Tn P X Y) *)
(* Goal: False *)
          exists P; left; split; Col.
(* Goal: and (@Col Tn P A B) (@Col Tn P X Y) *)
(* Goal: False *)
          exists B; right; right; split; Col.
(* Goal: and (@Col Tn P A B) (@Col Tn P X Y) *)
(* Goal: False *)
          exists A; right; right; split; Col.
(* Goal: and (@Col Tn P A B) (@Col Tn P X Y) *)
(* Goal: False *)
          exists P; left; split; Col.
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
          apply H4.
        eapply perp_col.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
          intro.
(* Goal: False *)
(* Goal: and (@OS Tn A C B D) (@OS Tn B D A C) *)
          subst D.
          assert (A = B).
            eapply symmetric_point_uniqueness.
              apply l7_2.
(* Goal: False *)
              apply H0.
            apply l7_2.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
            assumption.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
          auto.
(* Goal: @Perp Tn A C B P *)
(* Goal: not (@eq (@Tpoint Tn) T A) *)
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
          apply perp_sym.
          eapply perp_col.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
            intro.
(* Goal: False *)
(* Goal: @Col Tn D T C *)
(* Goal: @Col Tn D T B *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)) *)
(* Goal: @TS Tn A C B D *)
            treat_equalities.
            apply perp_distinct in H17.
(* Goal: @Perp Tn A C B P *)
            spliter.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
            auto.
(* Goal: @Perp Tn P Q P P' *)
(* Goal: not (@eq (@Tpoint Tn) Q P) *)
(* Goal: not (@eq (@Tpoint Tn) P P') *)
(* Goal: @Col Tn P P Q *)
            apply perp_left_comm.
            apply H17.
(* Goal: @Col Tn T A C *)
(* Goal: @Bet Tn B T D *)
(* Goal: @TS Tn A C B D *)
          apply bet_col in H7.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
          Col.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
        Col.
      apply perp_distinct in H17.
(* Goal: @Perp Tn A C B P *)
      spliter.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
      tauto.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
      intro.
(* Goal: False *)
(* Goal: @Col Tn D T C *)
(* Goal: @Col Tn D T B *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)) *)
(* Goal: @TS Tn A C B D *)
      treat_equalities.
(* Goal: @Perp Tn P Q P A *)
(* Goal: @Perp Tn P Q P A *)
(* Goal: not (@eq (@Tpoint Tn) Q P) *)
(* Goal: not (@eq (@Tpoint Tn) P A) *)
(* Goal: @Col Tn P P Q *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (not (@eq (@Tpoint Tn) C D)) (and (@Par Tn A B C D) (@Col Tn P C D)))) *)
      apply perp_distinct in H4.
(* Goal: @Perp Tn A C B P *)
      spliter.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
      tauto.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
    intro.
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
    subst C.
    assert(F = C').
      apply is_midpoint_id .
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      assumption.
(* Goal: False *)
(* Goal: @Col Tn D T C *)
(* Goal: @Col Tn D T B *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)) *)
(* Goal: @TS Tn A C B D *)
    treat_equalities.
    assert(A = E).
      eapply symmetric_point_uniqueness.
        apply l7_2.
(* Goal: False *)
        apply H0.
(* Goal: and (@Col Tn C D P) (@Perp_at Tn P A B C D) *)
      split.
(* Goal: @Bet Tn B T D *)
(* Goal: @TS Tn A C B D *)
        apply between_symmetry.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
        assumption.
      Cong.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
    tauto.
Qed.

Lemma l12_18_a :
  forall A B C D P,
  Cong A B C D -> Cong B C D A -> ~Col A B C ->
  B <> D -> Col A P C -> Col B P D ->
  Par A B C D.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
    assert(Midpoint P A C /\ Midpoint P B D) by (apply l7_21; assumption).
(* Goal: @Perp Tn A C B P *)
    spliter.
    eapply l12_17.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
      intro.
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
      subst B.
(* Goal: @CongA Tn A B P C B P *)
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
      apply H1.
(* Goal: @Col Tn A A B *)
(* Goal: @Col Tn A C D *)
(* Goal: @Col Tn D T C *)
(* Goal: @Col Tn D T B *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)) *)
(* Goal: @TS Tn A C B D *)
      apply col_trivial_1.
(* Goal: False *)
(* Goal: False *)
      apply H5.
    apply H6.
Qed.

Lemma l12_18_b :
  forall A B C D P,
  Cong A B C D -> Cong B C D A -> ~Col A B C ->
  B <> D -> Col A P C -> Col B P D ->
  Par B C D A.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
    assert(Midpoint P A C /\ Midpoint P B D) by (apply l7_21; assumption).
    eapply l12_18_a.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      assumption.
      Cong.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
      intro.
(* Goal: @CongA Tn A B P C B P *)
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
      apply H1.
      assert(Col B C P).
        eapply col_transitivity_1.
(* Goal: @Perp Tn A B P P' *)
(* Goal: @Perp Tn P Q P P' *)
(* Goal: @Col Tn P P Q *)
          apply H2.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
          Col.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
        Col.
(* Goal: @Col Tn C B D *)
      apply col_permutation_1.
      eapply (col_transitivity_1 _ P).
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
        intro.
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
        subst P.
(* Goal: @Perp Tn A C B P *)
        spliter.
        apply l7_2 in H5.
        apply is_midpoint_id in H5.
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
        subst C.
(* Goal: @CongA Tn A B P C B P *)
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
        apply H1.
(* Goal: @Col Tn B A B *)
        apply col_trivial_3.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
        Col.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
      Col.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
      intro.
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
      subst C.
(* Goal: @CongA Tn A B P C B P *)
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
      apply H1.
(* Goal: @Col Tn B A B *)
      apply col_trivial_3.
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
      apply H4.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
    Col.
Qed.

Lemma l12_18_c :
 forall A B C D P,
  Cong A B C D -> Cong B C D A -> ~Col A B C ->
  B <> D -> Col A P C -> Col B P D ->
  TS B D A C.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
    assert(Midpoint P A C /\ Midpoint P B D) by (apply l7_21; assumption).
    unfold TS.
(* Goal: and (not (@Col Tn B A C)) (and (not (@Col Tn D A C)) (@ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)))) *)
(* Goal: @TS Tn A C B D *)
    repeat split.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
      intro.
(* Goal: @CongA Tn A B P C B P *)
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
      apply H1.
      assert(Col A B P).
(* Goal: @Col Tn T C D *)
(* Goal: False *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)) *)
(* Goal: @TS Tn A C B D *)
        apply col_permutation_2.
        eapply (col_transitivity_1 _ D).
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
          assumption.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
          Col.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
        Col.
      eapply (col_transitivity_1 _ P).
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
        intro.
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
        subst P.
(* Goal: @Perp Tn A C B P *)
        spliter.
        apply is_midpoint_id in H5.
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
        subst C.
(* Goal: @CongA Tn A B P C B P *)
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
        apply H1.
(* Goal: @Col Tn B A B *)
        apply col_trivial_3.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
        Col.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
      Col.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
      intro.
(* Goal: @CongA Tn A B P C B P *)
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
      apply H1.
      assert(Col B P C).
        eapply (col_transitivity_1 _ D).
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
          assumption.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
          Col.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
        Col.
(* Goal: @Col Tn C B D *)
      apply col_permutation_1.
      eapply (col_transitivity_1 _ P).
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
        intro.
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
        subst P.
(* Goal: @Perp Tn A C B P *)
        spliter.
        apply l7_2 in H5.
        apply is_midpoint_id in H5.
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
        subst C.
(* Goal: @CongA Tn A B P C B P *)
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
        apply H1.
(* Goal: @Col Tn B A B *)
        apply col_trivial_3.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
        Col.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
      Col.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn A B P) (and (@Col Tn C D P) (@Perp_at Tn P A B C D))) *)
    exists P.
(* Goal: and (@Col Tn C D P) (@Perp_at Tn P A B C D) *)
    split.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
      Col.
(* Goal: @Perp Tn A C B P *)
    spliter.
    unfold Midpoint in H5.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
    tauto.
Qed.

Lemma l12_18_d :
 forall A B C D P,
 Cong A B C D -> Cong B C D A -> ~Col A B C ->
 B <> D -> Col A P C -> Col B P D ->
 TS A C B D.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
    assert(Midpoint P A C /\ Midpoint P B D) by (apply l7_21; assumption).
    eapply (l12_18_c _ _ _ _ P).
      Cong.
      Cong.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
      intro.
(* Goal: @CongA Tn A B P C B P *)
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
      apply H1.
      assert(Col A B P).
(* Goal: @Col Tn T C D *)
(* Goal: False *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)) *)
(* Goal: @TS Tn A C B D *)
        eapply col_permutation_2.
        eapply col_transitivity_1.
(* Goal: @Perp Tn A B P P' *)
(* Goal: @Perp Tn P Q P P' *)
(* Goal: @Col Tn P P Q *)
          apply H2.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
          Col.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
        Col.
      eapply (col_transitivity_1 _ P).
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
        intro.
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
        subst P.
(* Goal: @Perp Tn A C B P *)
        spliter.
        apply is_midpoint_id in H5.
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
        subst C.
(* Goal: False *)
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
        contradiction.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
        Col.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
      Col.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
      intro.
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
      subst C.
(* Goal: @CongA Tn A B P C B P *)
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
      apply H1.
(* Goal: @Col Tn B A B *)
      apply col_trivial_3.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
      Col.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
    Col.
Qed.

Lemma l12_18 :
 forall A B C D P,
  Cong A B C D -> Cong B C D A -> ~Col A B C ->
  B <> D -> Col A P C -> Col B P D ->
  Par A B C D /\ Par B C D A /\ TS B D A C /\ TS A C B D.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: and (@Col Tn C D P) (@Perp_at Tn P A B C D) *)
    split.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      apply (l12_18_a _ _ _ _ P); assumption.
(* Goal: and (@Col Tn C D P) (@Perp_at Tn P A B C D) *)
    split.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      apply (l12_18_b _ _ _ _ P); assumption.
(* Goal: and (@Col Tn C D P) (@Perp_at Tn P A B C D) *)
    split.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      apply (l12_18_c _ _ _ _ P); assumption.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
    apply (l12_18_d _ _ _ _ P); assumption.
Qed.

Lemma par_two_sides_two_sides :
  forall A B C D,
  Par A B C D -> TS B D A C ->
  TS A C B D.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: @TS Tn A C B D *)
    apply par_distincts in H.
(* Goal: @Perp Tn A C B P *)
    spliter.
(* Goal: @TS Tn A C B D *)
    unfold Par in H.
(* Goal: @TS Tn A C B D *)
    induction H.
(* Goal: @Perp Tn A C B P *)
      assert(A <> C).
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
        intro.
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
        subst C.
(* Goal: and (@OS Tn A C B D) (@OS Tn B D A C) *)
        unfold Par_strict in H.
(* Goal: @Perp Tn A C B P *)
        spliter.
(* Goal: False *)
(* Goal: False *)
        apply H5.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A B) (@Col Tn X C D)) *)
(* Goal: @OS Tn B D A C *)
        exists A.
(* Goal: @Col Tn A A B *)
(* Goal: @Col Tn A C D *)
(* Goal: @Col Tn D T C *)
(* Goal: @Col Tn D T B *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)) *)
(* Goal: @TS Tn A C B D *)
        split; apply col_trivial_1.
(* Goal: @TS Tn A C B D *)
(* Goal: @TS Tn A C B D *)
      unfold TS in *.
(* Goal: and (not (@Col Tn B A C)) (and (not (@Col Tn D A C)) (@ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)))) *)
(* Goal: @TS Tn A C B D *)
      assert (~ Col A B D).
(* Goal: @Perp Tn A C B P *)
        spliter.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
        assumption.
(* Goal: @Perp Tn A C B P *)
      spliter.
(* Goal: and (not (@Col Tn B A C)) (and (not (@Col Tn D A C)) (@ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)))) *)
(* Goal: @TS Tn A C B D *)
      ex_and H6 T.
(* Goal: and (not (@Col Tn B A C)) (and (not (@Col Tn D A C)) (@ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)))) *)
(* Goal: @TS Tn A C B D *)
      repeat split.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
        intro.
(* Goal: False *)
(* Goal: not (@Col Tn D A C) *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)) *)
(* Goal: @TS Tn A C B D *)
        assert(Col T B C).
(* Goal: @Col Tn C B D *)
          apply col_permutation_1.
(* Goal: @Col Tn C T B *)
(* Goal: False *)
(* Goal: not (@Col Tn D A C) *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)) *)
(* Goal: @TS Tn A C B D *)
          eapply (col_transitivity_1 _ A).
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
            auto.
(* Goal: @Col Tn T A C *)
(* Goal: @Bet Tn B T D *)
(* Goal: @TS Tn A C B D *)
            apply bet_col in H7.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
            Col.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
          Col.
(* Goal: False *)
(* Goal: False *)
        apply H5.
(* Goal: @Col Tn T C D *)
(* Goal: False *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)) *)
(* Goal: @TS Tn A C B D *)
        apply col_permutation_2.
(* Goal: @Col Tn B D C *)
(* Goal: not (@Col Tn D A C) *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)) *)
(* Goal: @TS Tn A C B D *)
        eapply (col_transitivity_1 _ T).
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
          intro.
(* Goal: False *)
(* Goal: @Col Tn D T C *)
(* Goal: @Col Tn D T B *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)) *)
(* Goal: @TS Tn A C B D *)
          treat_equalities.
(* Goal: and (@OS Tn A C B D) (@OS Tn B D A C) *)
          unfold Par_strict in H.
(* Goal: @Perp Tn A C B P *)
          spliter.
(* Goal: False *)
(* Goal: @Col Tn D T C *)
(* Goal: @Col Tn D T B *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)) *)
(* Goal: @TS Tn A C B D *)
          apply H9.
(* Goal: @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => and (@Midpoint Tn T A C') (@Cong Tn B A B C')) *)
(* Goal: @Perp Tn A C B P *)
          exists C.
(* Goal: and (@Col Tn C D P) (@Perp_at Tn P A B C D) *)
          split.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
            Col.
(* Goal: @Col Tn A A B *)
(* Goal: @Col Tn A C D *)
(* Goal: @Col Tn D T C *)
(* Goal: @Col Tn D T B *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)) *)
(* Goal: @TS Tn A C B D *)
          apply col_trivial_1.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
          Col.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
        Col.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
        intro.
(* Goal: False *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)) *)
(* Goal: @TS Tn A C B D *)
        assert(Col T C D).
(* Goal: @Col Tn T C D *)
(* Goal: False *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)) *)
(* Goal: @TS Tn A C B D *)
          apply col_permutation_2.
(* Goal: @Col Tn C D T *)
(* Goal: False *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)) *)
(* Goal: @TS Tn A C B D *)
          apply (col_transitivity_1 _ A).
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
            auto.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
            Col.
(* Goal: @Col Tn T A C *)
(* Goal: @Bet Tn B T D *)
(* Goal: @TS Tn A C B D *)
          apply bet_col in H7.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
          Col.
(* Goal: False *)
(* Goal: False *)
        apply H5.
(* Goal: @Col Tn C B D *)
        apply col_permutation_1.
(* Goal: @Col Tn D C B *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)) *)
(* Goal: @TS Tn A C B D *)
        apply (col_transitivity_1 _ T).
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
          intro.
(* Goal: False *)
(* Goal: @Col Tn D T C *)
(* Goal: @Col Tn D T B *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)) *)
(* Goal: @TS Tn A C B D *)
          treat_equalities.
(* Goal: and (@OS Tn A C B D) (@OS Tn B D A C) *)
          unfold Par_strict in H.
(* Goal: @Perp Tn A C B P *)
          spliter.
(* Goal: False *)
(* Goal: @Col Tn D T C *)
(* Goal: @Col Tn D T B *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)) *)
(* Goal: @TS Tn A C B D *)
          apply H9.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A B) (@Col Tn X C D)) *)
(* Goal: @OS Tn B D A C *)
          exists A.
(* Goal: and (@Col Tn C D P) (@Perp_at Tn P A B C D) *)
          split.
(* Goal: @Col Tn A A B *)
(* Goal: @Col Tn A C D *)
(* Goal: @Col Tn D T C *)
(* Goal: @Col Tn D T B *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)) *)
(* Goal: @TS Tn A C B D *)
            apply col_trivial_1.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
          Col.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
          Col.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
        Col.
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)) *)
(* Goal: @TS Tn A C B D *)
      exists T.
(* Goal: and (@Col Tn C D P) (@Perp_at Tn P A B C D) *)
      split.
(* Goal: @Col Tn T A C *)
(* Goal: @Bet Tn B T D *)
(* Goal: @TS Tn A C B D *)
        apply bet_col in H7.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
        Col.
(* Goal: @Bet Tn B T D *)
(* Goal: @TS Tn A C B D *)
      unfold Col in H6.
(* Goal: @Bet Tn B T D *)
(* Goal: @TS Tn A C B D *)
      induction H6.
(* Goal: @Bet Tn B T D *)
(* Goal: @Bet Tn B T D *)
(* Goal: @TS Tn A C B D *)
        assert(HH:= outer_pasch C D T A B (between_symmetry _ _ _ H7) (between_symmetry _ _ _ H6)).
(* Goal: @Bet Tn B T D *)
(* Goal: @Bet Tn B T D *)
(* Goal: @TS Tn A C B D *)
        ex_and HH X.
(* Goal: and (@OS Tn A C B D) (@OS Tn B D A C) *)
        unfold Par_strict in H.
(* Goal: @Perp Tn A C B P *)
        spliter.
(* Goal: @TS Tn A C B D *)
        apply False_ind.
(* Goal: False *)
(* Goal: @Bet Tn B T D *)
(* Goal: @TS Tn A C B D *)
        apply H12.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A B) (@Col Tn X C D)) *)
(* Goal: @Bet Tn B T D *)
(* Goal: @TS Tn A C B D *)
        exists X.
(* Goal: and (@Col Tn X A B) (@Col Tn X C D) *)
(* Goal: @Bet Tn B T D *)
(* Goal: @TS Tn A C B D *)
        apply bet_col in H8.
(* Goal: and (@Col Tn X A B) (@Col Tn X C D) *)
(* Goal: @Bet Tn B T D *)
(* Goal: @TS Tn A C B D *)
        apply bet_col in H9.
(* Goal: and (@Col Tn P A B) (@Col Tn P X Y) *)
(* Goal: False *)
        split; Col.
(* Goal: @Bet Tn B T D *)
(* Goal: @TS Tn A C B D *)
      induction H6.
(* Goal: @Bet Tn B T D *)
(* Goal: @Bet Tn B T D *)
(* Goal: @TS Tn A C B D *)
        assert(HH:= outer_pasch A B T C D H7 H6).
(* Goal: @Bet Tn B T D *)
(* Goal: @Bet Tn B T D *)
(* Goal: @TS Tn A C B D *)
        ex_and HH X.
(* Goal: @TS Tn A C B D *)
        apply False_ind.
(* Goal: and (@OS Tn A C B D) (@OS Tn B D A C) *)
        unfold Par_strict in H.
(* Goal: @Perp Tn A C B P *)
        spliter.
(* Goal: False *)
(* Goal: @Bet Tn B T D *)
(* Goal: @TS Tn A C B D *)
        apply H12.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A B) (@Col Tn X C D)) *)
(* Goal: @Bet Tn B T D *)
(* Goal: @TS Tn A C B D *)
        exists X.
(* Goal: and (@Col Tn X A B) (@Col Tn X C D) *)
(* Goal: @Bet Tn B T D *)
(* Goal: @TS Tn A C B D *)
        apply bet_col in H8.
(* Goal: and (@Col Tn X A B) (@Col Tn X C D) *)
(* Goal: @Bet Tn B T D *)
(* Goal: @TS Tn A C B D *)
        apply bet_col in H9.
(* Goal: and (@Col Tn P A B) (@Col Tn P X Y) *)
(* Goal: False *)
        split; Col.
(* Goal: @Bet Tn B T D *)
(* Goal: @TS Tn A C B D *)
      apply between_symmetry.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      assumption.
(* Goal: @TS Tn A C B D *)
    unfold TS in H0.
(* Goal: @Perp Tn A C B P *)
    spliter.
(* Goal: @TS Tn A C B D *)
    apply False_ind.
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
    apply H3.
(* Goal: @Col Tn C B D *)
    apply col_permutation_1.
(* Goal: @Col Tn D C B *)
    eapply (col_transitivity_1 _ C).
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
      auto.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
      Col.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
    Col.
Qed.

Lemma par_one_or_two_sides :
 forall A B C D,
  Par_strict A B C D ->
 TS A C B D /\ TS B D A C \/ OS A C B D /\ OS B D A C.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: or (and (@TS Tn A C B D) (@TS Tn B D A C)) (and (@OS Tn A C B D) (@OS Tn B D A C)) *)
    induction(two_sides_dec A C B D).
(* Goal: or (@Bet Tn B P T) (@Bet Tn B T P) *)
(* Goal: or (@Bet Tn B P T) (@Bet Tn B T P) *)
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
      left.
(* Goal: and (@Col Tn C D P) (@Perp_at Tn P A B C D) *)
      split.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
        assumption.
(* Goal: @TS Tn A C B D *)
      apply par_two_sides_two_sides.
(* Goal: @Par Tn B A D C *)
(* Goal: @TS Tn A C B D *)
(* Goal: or (and (@TS Tn A C B D) (@TS Tn B D A C)) (and (@OS Tn A C B D) (@OS Tn B D A C)) *)
        apply par_comm.
(* Goal: @Par Tn A B B C *)
        unfold Par.
(* Goal: or (@Bet Tn B P T) (@Bet Tn B T P) *)
(* Goal: or (@Bet Tn B P T) (@Bet Tn B T P) *)
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
        left.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
        assumption.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      assumption.
(* Goal: or (@Bet Tn B P T) (@Bet Tn B T P) *)
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
    right.
(* Goal: @Perp Tn A C B P *)
    assert(HH:=H).
(* Goal: and (@OS Tn A C B D) (@OS Tn B D A C) *)
    unfold Par_strict in H.
(* Goal: @Perp Tn A C B P *)
    spliter.
(* Goal: @Perp Tn A C B P *)
    assert(A <> C).
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
      intro.
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
      subst C.
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
      apply H3.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A B) (@Col Tn X C D)) *)
(* Goal: @OS Tn B D A C *)
      exists A.
(* Goal: and (@Col Tn P A B) (@Col Tn P X Y) *)
(* Goal: False *)
      split; Col.
(* Goal: and (@OS Tn A C B D) (@OS Tn B D A C) *)
    assert(B <> D).
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
      intro.
(* Goal: False *)
(* Goal: and (@OS Tn A C B D) (@OS Tn B D A C) *)
      subst D.
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
      apply H3.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A B) (@Col Tn X C D)) *)
(* Goal: not (@TS Tn B D A C) *)
      exists B.
(* Goal: and (@Col Tn P A B) (@Col Tn P X Y) *)
(* Goal: False *)
      split; Col.
(* Goal: and (@Col Tn C D P) (@Perp_at Tn P A B C D) *)
    split.
(* Goal: @Coplanar Tn P P' A Q *)
(* Goal: @Coplanar Tn P P' B P *)
(* Goal: @Coplanar Tn P P' B Q *)
(* Goal: @Perp Tn A B P P' *)
(* Goal: @Perp Tn P Q P P' *)
(* Goal: @Col Tn P P Q *)
      apply cop__not_two_sides_one_side; Cop.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
        intro.
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
        apply H3.
(* Goal: @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => and (@Midpoint Tn T A C') (@Cong Tn B A B C')) *)
(* Goal: @Perp Tn A C B P *)
        exists C.
(* Goal: and (@Col Tn P A B) (@Col Tn P X Y) *)
(* Goal: False *)
        split; Col.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
        intro.
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
        apply H3.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A B) (@Col Tn X C D)) *)
(* Goal: @OS Tn B D A C *)
        exists A.
(* Goal: and (@Col Tn P A B) (@Col Tn P X Y) *)
(* Goal: False *)
        split; Col.
(* Goal: @Coplanar Tn P P' A Q *)
(* Goal: @Coplanar Tn P P' B P *)
(* Goal: @Coplanar Tn P P' B Q *)
(* Goal: @Perp Tn A B P P' *)
(* Goal: @Perp Tn P Q P P' *)
(* Goal: @Col Tn P P Q *)
    apply cop__not_two_sides_one_side; Cop.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
      intro.
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
      apply H3.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A B) (@Col Tn X C D)) *)
(* Goal: not (@Col Tn C B D) *)
(* Goal: not (@TS Tn B D A C) *)
      exists D.
(* Goal: and (@Col Tn P A B) (@Col Tn P X Y) *)
(* Goal: False *)
      split; Col.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
      intro.
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
      apply H3.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A B) (@Col Tn X C D)) *)
(* Goal: not (@TS Tn B D A C) *)
      exists B.
(* Goal: and (@Col Tn P A B) (@Col Tn P X Y) *)
(* Goal: False *)
      split; Col.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
    intro.
(* Goal: False *)
    apply H0.
(* Goal: @TS Tn A C B D *)
    apply par_two_sides_two_sides.
(* Goal: or (@Bet Tn B P T) (@Bet Tn B T P) *)
(* Goal: or (@Bet Tn B P T) (@Bet Tn B T P) *)
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
      left.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      assumption.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
    assumption.
Qed.

Lemma l12_21_b : forall A B C D,
 TS A C B D ->
 CongA B A C D C A -> Par A B C D.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
    apply conga_distinct in H0.
(* Goal: @Perp Tn A C B P *)
    spliter.
    assert(~Col A B C).
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
      intro.
      unfold TS in H.
(* Goal: @Perp Tn A C B P *)
      spliter.
      apply col_permutation_4 in H5.
      assert(Col D C A).
        eapply col_conga_col.
(* Goal: False *)
(* Goal: False *)
          apply H5.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
        assumption.
(* Goal: False *)
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
      contradiction.
    assert(A <> B /\ C <> D).
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
      auto.
(* Goal: @Perp Tn A C B P *)
    spliter.
    assert(HH:=segment_construction_3 C D A B H7 H6).
    ex_and HH D'.
    assert(CongA B A C D' C A).
      eapply l11_10.
(* Goal: False *)
        apply H0.
(* Goal: @Out Tn B C C *)
(* Goal: @Perp Tn A C B P *)
        apply out_trivial.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
        assumption.
(* Goal: @Out Tn B C C *)
(* Goal: @Perp Tn A C B P *)
        apply out_trivial.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
        assumption.
        apply l6_6.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
        assumption.
(* Goal: @Out Tn B C C *)
(* Goal: @Perp Tn A C B P *)
      apply out_trivial.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      assumption.
    assert(Cong D' A B C).
      eapply cong2_conga_cong.
        apply conga_sym.
(* Goal: False *)
(* Goal: @Col Tn T A C *)
        apply H10.
        Cong.
      Cong.
    assert(TS A C D' B).
      eapply l9_5.
        apply l9_2.
(* Goal: False *)
        apply H.
(* Goal: @Col Tn B A B *)
        apply col_trivial_3.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      assumption.
    unfold TS in H12.
(* Goal: @Perp Tn A C B P *)
    spliter.
    ex_and H14 M.
    assert(B <> D').
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
      intro.
(* Goal: False *)
(* Goal: @Col Tn D T C *)
(* Goal: @Col Tn D T B *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)) *)
(* Goal: @TS Tn A C B D *)
      treat_equalities.
(* Goal: False *)
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
      contradiction.
    assert(Midpoint M A C /\ Midpoint M B D').
      apply l7_21.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
        assumption.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
        assumption.
        Cong.
        Cong.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
        Col.
      apply bet_col in H15.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
      Col.
(* Goal: @Perp Tn A C B P *)
    spliter.
    assert(Par A B C D').
      eapply l12_17.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
        assumption.
        apply H17.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      assumption.
    eapply par_col_par.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
      auto.
      apply H19.
    apply out_col in H8.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
    Col.
Qed.

Lemma l12_22_aux :
 forall A B C D P,
  P <> A -> A <> C -> Bet P A C -> OS P A B D ->
  CongA B A P D C P ->
  Par A B C D.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
    assert (P<>C) by (intro; Between).
    prolong B A B' B A .
(* Goal: @Perp Tn A C B P *)
    spliter.
    assert(CongA P A B C A B').
      apply l11_14.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
        assumption.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
        assumption.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
        auto.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
        assumption.
        unfold CongA in H3.
(* Goal: @Perp Tn A C B P *)
        spliter.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
        auto.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
        intro.
(* Goal: False *)
(* Goal: @Col Tn D T C *)
(* Goal: @Col Tn D T B *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)) *)
(* Goal: @TS Tn A C B D *)
        treat_equalities.
        unfold CongA in H3.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
        tauto.
    assert(CongA D C A D C P).
      eapply l11_10.
        apply conga_refl.
(* Goal: @Out Tn B C C *)
(* Goal: @Perp Tn A C B P *)
          3: apply out_trivial.
          unfold CongA in H3.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
          tauto.
(* Goal: @Out Tn B C C *)
(* Goal: @Perp Tn A C B P *)
        5:apply out_trivial.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
        auto.
        unfold CongA in H3.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
        tauto.
        apply between_symmetry in H1.
        apply bet_out in H1.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
          assumption.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
          auto.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
          auto.
(* Goal: @Out Tn B C C *)
(* Goal: @Perp Tn A C B P *)
        apply out_trivial.
        unfold CongA in H3.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
        tauto.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
      auto.
    assert(Par A B' C D).
      eapply l12_21_b.
        assert(~Col B P A).
          unfold OS in H2.
          ex_and H2 T.
          unfold TS in H2.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
          tauto.
        assert(TS P A B B').
          unfold TS.
(* Goal: and (not (@Col Tn B A C)) (and (not (@Col Tn D A C)) (@ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)))) *)
(* Goal: @TS Tn A C B D *)
          repeat split.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
            assumption.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
            intro.
(* Goal: False *)
(* Goal: @Col Tn D T C *)
(* Goal: @Col Tn D T B *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)) *)
(* Goal: @TS Tn A C B D *)
            apply H9.
(* Goal: @Col Tn C B D *)
            apply col_permutation_1.
            eapply (col_transitivity_1 _ B').
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
              intro.
(* Goal: False *)
(* Goal: @Col Tn D T C *)
(* Goal: @Col Tn D T B *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)) *)
(* Goal: @TS Tn A C B D *)
              treat_equalities.
              unfold CongA in H3.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
              tauto.
              apply bet_col in H1.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
              Col.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
            Col.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A B) (@Col Tn X C D)) *)
(* Goal: @OS Tn B D A C *)
          exists A.
(* Goal: and (@Col Tn C D P) (@Perp_at Tn P A B C D) *)
          split.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
            Col.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
          assumption.
        apply l9_2.
        eapply l9_8_2.
          eapply col_two_sides.
            3:apply invert_two_sides.
(* Goal: False *)
(* Goal: @Col Tn T A C *)
            3: apply H10.
            apply bet_col in H1.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
            Col.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
          assumption.
        eapply col_one_side.
          3: apply invert_one_side.
(* Goal: @Perp Tn A B P P' *)
(* Goal: @Perp Tn P Q P P' *)
(* Goal: @Col Tn P P Q *)
          3: apply H2.
          apply bet_col in H1.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
          Col.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
        assumption.
      eapply conga_trans.
        apply conga_sym.
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
        apply conga_comm.
        apply H7.
      eapply conga_trans.
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
        apply H3.
      apply conga_sym.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      assumption.
(* Goal: @Par Tn E F C D *)
    apply par_symmetry.
    eapply par_col_par.
(* Goal: @Par Tn E F C D *)
      2: apply par_symmetry.
(* Goal: False *)
(* Goal: @Col Tn D T C *)
(* Goal: @Col Tn D T B *)
(* Goal: @ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)) *)
(* Goal: @TS Tn A C B D *)
      2:apply H9.
      unfold CongA in H3.
(* Goal: @Perp Tn A C B P *)
      spliter.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
      auto.
    apply bet_col in H1.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
    Col.
Qed.


Lemma l12_22_b :
 forall A B C D P,
  Out P A C -> OS P A B D -> CongA B A P D C P ->
  Par A B C D.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
    induction(eq_dec_points A C).
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
      subst C.
(* Goal: @Par Tn A B B C *)
      unfold Par.
(* Goal: or (@Bet Tn B P T) (@Bet Tn B T P) *)
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
      right.
(* Goal: and (not (@Col Tn B A C)) (and (not (@Col Tn D A C)) (@ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T A C) (@Bet Tn B T D)))) *)
(* Goal: @TS Tn A C B D *)
      repeat split.
        unfold CongA in H1.
(* Goal: @Perp Tn A C B P *)
        spliter.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
        auto.
        unfold CongA in H1.
(* Goal: @Perp Tn A C B P *)
        spliter.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
        auto.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
        Col.
      apply conga_comm in H1.
(* Goal: @Coplanar Tn P P' A Q *)
(* Goal: @Coplanar Tn P P' B P *)
(* Goal: @Coplanar Tn P P' B Q *)
(* Goal: @Perp Tn A B P P' *)
(* Goal: @Perp Tn P Q P P' *)
(* Goal: @Col Tn P P Q *)
      apply conga_cop__or_out_ts in H1; Cop.
(* Goal: False *)
      induction H1.
        apply out_col in H1.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
        Col.
      apply l9_9 in H1.
(* Goal: False *)
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
      contradiction.
    unfold Out in H.
(* Goal: @Perp Tn A C B P *)
    spliter.
(* Goal: @Perp Tn P Q P A *)
(* Goal: not (@eq (@Tpoint Tn) Q P) *)
(* Goal: not (@eq (@Tpoint Tn) P A) *)
(* Goal: @Col Tn P P Q *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (not (@eq (@Tpoint Tn) C D)) (and (@Par Tn A B C D) (@Col Tn P C D)))) *)
    induction H4.
      eapply l12_22_aux.
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
        3:apply H4.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
        auto.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
        assumption.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
        assumption.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      assumption.
(* Goal: @Par Tn E F C D *)
    apply par_symmetry.
    eapply l12_22_aux.
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
      3:apply H4.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
      auto.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
      auto.
      eapply (col_one_side _ A).
        apply bet_col in H4.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
        Col.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
        auto.
      apply one_side_symmetry.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      assumption.
    apply conga_sym.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
    assumption.
Qed.

Lemma par_strict_par : forall A B C D,
 Par_strict A B C D -> Par A B C D.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: @Par Tn A B B C *)
    unfold Par.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
    tauto.
Qed.


Lemma par_strict_distinct : forall A B C D,
 Par_strict A B C D ->
  A<>B /\ A<>C /\ A<>D /\ B<>C /\ B<>D /\ C<>D.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Par_strict Tn A B C D), and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) A C)) (and (not (@eq (@Tpoint Tn) A D)) (and (not (@eq (@Tpoint Tn) B C)) (and (not (@eq (@Tpoint Tn) B D)) (not (@eq (@Tpoint Tn) C D)))))) *)
    unfold Par_strict.
(* Goal: @Perp Tn A C B P *)
    intros; spliter.
    repeat split; auto;
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A B) (@Col Tn X C D)) *)
(* Goal: @OS Tn B D A C *)
    intro; apply H2; [exists A..|exists B|exists B]; subst; split; Col.
Qed.

Lemma col_par : forall A B C,
 A <> B -> B <> C ->
 Col A B C -> Par A B B C.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: @Par Tn A B B C *)
    unfold Par.
(* Goal: or (@Bet Tn B P T) (@Bet Tn B T P) *)
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
    right.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
    intuition Col.
Qed.

Lemma acute_col_perp__out : forall A B C A',
  Acute A B C -> Col B C A' -> Perp B C A A' -> Out B A' C.
Proof.
(* Goal: forall (A B C A' : @Tpoint Tn) (_ : @Acute Tn A B C) (_ : @Col Tn B C A') (_ : @Perp Tn B C A A'), @Out Tn B A' C *)
  intros A B C A' HacuteB HBCA' HPerp.
(* Goal: @Out Tn B A' C *)
  assert(HUn := perp_not_col2 B C A A' HPerp).
(* Goal: @Out Tn B A' C *)
  destruct HUn as [HNCol1|]; [|contradiction].
(* Goal: @Out Tn B A' C *)
  assert(HB' := l10_15 B C B A).
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
  destruct HB' as [B' []]; Col.
(* Goal: @InAngle Tn P A B C *)
  assert_diffs.
(* Goal: @Out Tn B A' C *)
  assert(HNCol2 : ~ Col B' B C ) by (apply per_not_col; Perp).
(* Goal: @Out Tn B A' C *)
  assert(HNCol3 : ~ Col B B' A).
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
  { intro.
(* Goal: False *)
    apply (nlta A B C).
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
    apply acute_per__lta; auto.
(* Goal: @Per Tn A B C *)
    apply (l8_3 B'); Col; Perp.
  }
(* Goal: @Out Tn B A' C *)
  assert(HPars : Par_strict B B' A A').
(* Goal: @Coplanar Tn P P' A Q *)
(* Goal: @Coplanar Tn P P' B P *)
(* Goal: @Coplanar Tn P P' B Q *)
(* Goal: @Perp Tn A B P P' *)
(* Goal: @Perp Tn P Q P P' *)
(* Goal: @Col Tn P P Q *)
    apply (par_not_col_strict _ _ _ _ A); Col; apply (l12_9 _ _ _ _ B C); Perp; Cop.
(* Goal: @Out Tn B A' C *)
  assert(HNCol4 := par_strict_not_col_4 B B' A A' HPars).
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
  apply (col_one_side_out _ B'); Col.
(* Goal: @OS Tn B B' A' C *)
  apply (one_side_transitivity _ _ _ A).
(* Goal: @Par Tn A B A B *)
(* Goal: @Col Tn P A B *)
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (not (@eq (@Tpoint Tn) C D)) (and (@Par Tn A B C D) (@Col Tn P C D)))) *)
    apply l12_6; Par.
(* Goal: @OS Tn B B' A C *)
  apply invert_one_side.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
  apply in_angle_one_side; Col.
(* Goal: @InAngle Tn A B' B C *)
  apply l11_24.
(* Goal: @InAngle Tn A C B B' *)
  apply lea_in_angle; Side.
(* Goal: @LeA Tn C B A C B B' *)
  apply lta_comm.
(* Goal: @LtA Tn A B C B' B C *)
  apply acute_per__lta; Perp.
Qed.

Lemma acute_col_perp__out_1 : forall A B C A',
  Acute A B C -> Col B C A' -> Perp B A A A' -> Out B A' C.
Proof.
(* Goal: forall (A B C A' : @Tpoint Tn) (_ : @Acute Tn A B C) (_ : @Col Tn B C A') (_ : @Perp Tn B A A A'), @Out Tn B A' C *)
  intros A B C A' HAcute HCol HPerp.
(* Goal: @Out Tn B A' C *)
  destruct (segment_construction A B A B) as [A0 [HA1 HA2]].
(* Goal: @Out Tn B A' C *)
  destruct (segment_construction C B C B) as [C0 [HC1 HC2]].
(* Goal: @InAngle Tn P A B C *)
  assert_diffs.
(* Goal: @Out Tn B A' C *)
  assert (HNCol : ~ Col B A A') by (apply per_not_col; Perp).
(* Goal: @InAngle Tn P A B C *)
  assert_diffs.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
  apply l6_2 with C0; auto.
(* Goal: @Bet Tn A' B C0 *)
  apply not_out_bet.
(* Goal: @Col Tn A B X *)
    ColR.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
  intro.
(* Goal: False *)
  apply (not_bet_and_out A B A0); split; trivial.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
  apply acute_col_perp__out with A'; Col.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
    apply acute_sym, (acute_conga__acute A B C); auto.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
    apply l11_14; auto.
(* Goal: @Bet Tn C B A' *)
(* Goal: @Perp Tn B A0 A' A *)
    apply between_symmetry, l6_2 with C0; Between.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
    apply l6_6; assumption.
(* Goal: @Perp Tn B A0 A' A *)
  apply perp_col with A; Col; Perp.
Qed.

Lemma conga_cop_inangle_per2__inangle : forall A B C P T,
  Per A B C -> InAngle T A B C -> CongA P B A P B C -> Per B P T -> Coplanar A B C P ->
  InAngle P A B C.
Proof.
(* Goal: @Coplanar Tn P P' A Q *)
(* Goal: @Coplanar Tn P P' B P *)
(* Goal: @Coplanar Tn P P' B Q *)
(* Goal: @Perp Tn A B P P' *)
(* Goal: @Perp Tn P Q P P' *)
(* Goal: @Col Tn P P Q *)
  intros A B C P T HPer HInangle HConga HPerP HCop.
(* Goal: @InAngle Tn P A B C *)
  destruct (eq_dec_points P T).
(* Goal: @InAngle Tn P A B C *)
(* Goal: @InAngle Tn P A B C *)
    subst; apply HInangle.
(* Goal: @InAngle Tn P A B C *)
  assert_diffs.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
  destruct (angle_bisector A B C) as [P' [HInangle' HConga']]; auto.
(* Goal: @InAngle Tn P A B C *)
  assert_diffs.
(* Goal: @InAngle Tn P A B C *)
  assert (HAcute : Acute P' B A).
(* Goal: @Acute Tn P' B A *)
(* Goal: @InAngle Tn P A B C *)
    apply acute_sym, conga_inangle_per__acute with C; trivial.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
  apply l11_25 with P' A C; try (apply out_trivial); auto.
(* Goal: @Out Tn B P P' *)
  assert (HNCol1 : ~ Col A B C) by (apply per_not_col; auto).
(* Goal: @Out Tn B P P' *)
  assert (HCol : Col B P P').
(* Goal: @Col Tn B P P' *)
(* Goal: @Out Tn B P P' *)
    apply conga2_cop2__col with A C; trivial.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
    intro; apply HNCol1; Col.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
    apply coplanar_trans_1 with C; Cop; Col.
(* Goal: @Coplanar Tn P P' A Q *)
(* Goal: @Coplanar Tn P P' B P *)
(* Goal: @Coplanar Tn P P' B Q *)
(* Goal: @Perp Tn A B P P' *)
(* Goal: @Perp Tn P Q P P' *)
(* Goal: @Col Tn P P Q *)
    apply coplanar_trans_1 with A; Cop.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
  apply (acute_col_perp__out T); Col.
(* Goal: @Acute Tn T B P' *)
(* Goal: @Perp Tn B P' T P *)
  { apply acute_lea_acute with P' B A; trivial.
(* Goal: @LeA Tn T B P' P' B A *)
    assert (HNCol2 : ~ Col P' B A).
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
      intro.
(* Goal: False *)
(* Goal: @LeA Tn T B P' P' B A *)
      assert (Col P' B C) by (apply (col_conga_col P' B A); assumption).
(* Goal: @Col Tn A B X *)
      apply HNCol1; ColR.
(* Goal: @LeA Tn T B P' P' B A *)
    assert (Coplanar A B T P') by (apply coplanar_trans_1 with C; Cop; Col).
(* Goal: @LeA Tn T B P' P' B A *)
    destruct (col_dec T B P'); [|assert_diffs; destruct (cop__one_or_two_sides B P' A T); Col; Cop].
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
    - apply l11_31_1; auto.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
      apply col_one_side_out with A; Col.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
      apply invert_one_side, inangle_one_side with C; Col.
(* Goal: not (@Col Tn A B T) *)
      assert (~ Col B P T) by (apply per_not_col; auto).
(* Goal: @Col Tn A B X *)
      intro; assert_diffs; apply HNCol2; ColR.
    - apply (l11_30 P' B T P' B C); CongA.
(* Goal: @LeA Tn T B P' P' B A *)
      exists T; split; CongA.
(* Goal: @InAngle Tn T P' B C *)
      apply l11_24 in HInangle; apply l11_24 in HInangle'.
(* Goal: @InAngle Tn T P' B C *)
      destruct (col_dec B C T).
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
        apply out341__inangle; auto.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
        apply col_in_angle_out with A; Col.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
        intro; apply HNCol1; Col.
(* Goal: @InAngle Tn T P' B C *)
      assert (HNCol3 : ~ Col P' B C) by (apply (ncol_conga_ncol P' B A); assumption).
(* Goal: @InAngle Tn T P' B C *)
      apply os2__inangle.
(* Goal: @OS Tn B P' C T *)
(* Goal: @OS Tn B C P' T *)
        exists A; split; Side.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
        apply invert_two_sides, in_angle_two_sides; Col.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
      apply invert_one_side, inangle_one_side with A; Col.
    - exists T; split; CongA.
(* Goal: @InAngle Tn T P' B A *)
      destruct (col_dec B A T).
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
        apply out341__inangle; auto.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
        apply col_in_angle_out with C; Col.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
        intro; apply HNCol1; Col.
(* Goal: @InAngle Tn T P' B A *)
      apply os2__inangle; trivial.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
      apply invert_one_side, inangle_one_side with C; Col.
  }
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
  apply perp_col with P; Col.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
  apply perp_right_comm, per_perp; auto.
Qed.

End T12_2'.

Hint Resolve col_par par_strict_par : par.

Hint Resolve l12_6 pars__os3412 : side.

(*
Ltac finish := repeat match goal with
 | |- Bet ?A ?B ?C => Between
 | |- Col ?A ?B ?C => Col
 | |- ~ Col ?A ?B ?C => Col
 | |- Par ?A ?B ?C ?D => Par
 | |- Par_strict ?A ?B ?C ?D => Par
 | |- Perp ?A ?B ?C ?D => Perp
 | |- Perp_at ?A ?B ?C ?D ?E => Perp
 | |- Per ?A ?B ?C => Perp
 | |- Cong ?A ?B ?C ?D => Cong
 | |- Midpoint ?A ?B ?C => Midpoint
 | |- ?A<>?B => apply swap_diff;assumption
 | |- _ => try assumption
end.
*)

Section T12_3.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma perp_not_par : forall A B X Y, Perp A B X Y -> ~ Par A B X Y.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: @Perp Tn A C B P *)
    assert(HH:=H).
(* Goal: not (@Par Tn A B X Y) *)
    unfold Perp in HH.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn A B P) (and (@Col Tn C D P) (@Perp_at Tn P A B C D))) *)
    ex_and HH P.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
    intro.
(* Goal: False *)
    induction H1.
(* Goal: @CongA Tn A B P C B P *)
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
      apply H1.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn A B P) (and (@Col Tn C D P) (@Perp_at Tn P A B C D))) *)
      exists P.
(* Goal: and (@Col Tn P A B) (@Col Tn P X Y) *)
(* Goal: False *)
      apply perp_in_col in H0.
(* Goal: @Perp Tn A C B P *)
      spliter.
(* Goal: and (@Col Tn P A B) (@Col Tn P X Y) *)
(* Goal: False *)
      split; Col.
(* Goal: @Perp Tn A C B P *)
    spliter.
(* Goal: False *)
    induction(eq_dec_points A Y).
(* Goal: False *)
(* Goal: False *)
      subst Y.
(* Goal: False *)
(* Goal: False *)
      assert(P = A).
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
        eapply (l8_14_2_1b P A B X A); Col.
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
      subst P.
(* Goal: False *)
(* Goal: False *)
      apply perp_in_comm in H0.
(* Goal: False *)
(* Goal: False *)
      apply perp_in_per in H0.
(* Goal: False *)
(* Goal: False *)
      assert(~ Col B A X).
(* Goal: not (@Col Tn B A X) *)
(* Goal: False *)
(* Goal: False *)
        eapply(per_not_col).
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
          auto.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
          auto.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
        assumption.
(* Goal: False *)
(* Goal: False *)
      apply H5.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
      Col.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
    apply(l8_16_1 A B X A Y); Col.
(* Goal: @Col Tn A B X *)
      ColR.
(* Goal: @Col Tn A B X *)
    ColR.
Qed.

Lemma cong_conga_perp : forall A B C P, TS B P A C -> Cong A B C B -> CongA A B P C B P -> Perp A C B P.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: @Perp Tn A C B P *)
    assert(HH:=H).
(* Goal: @Perp Tn A C B P *)
    unfold TS in HH.
(* Goal: @Perp Tn A C B P *)
    assert (~ Col A B P).
(* Goal: @Perp Tn A C B P *)
      spliter.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      assumption.
(* Goal: @Perp Tn A C B P *)
    spliter.
(* Goal: @Perp Tn A C B P *)
    ex_and H5 T.
(* Goal: @Perp Tn A C B P *)
    assert(B <> P).
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
      intro.
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
      subst P.
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
      apply H3.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
      Col.
(* Goal: @Perp Tn A C B P *)
    assert(A <> B).
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
      intro.
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
      subst B.
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
      apply H3.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
      Col.
(* Goal: @Perp Tn A C B P *)
    assert(C <> B).
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
      intro.
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
      subst C.
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
      apply H4.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
      Col.
(* Goal: @Perp Tn A C B P *)
    assert(A <> C).
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
      intro.
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
      subst C.
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
      assert(OS B P A A).
        apply one_side_reflexivity.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
        assumption.
(* Goal: False *)
(* Goal: @Perp Tn A C B P *)
      apply l9_9 in H.
(* Goal: False *)
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
      contradiction.
(* Goal: @Perp Tn A C B P *)
    induction (bet_dec A B C).
(* Goal: @Perp Tn A C B P *)
(* Goal: @Perp Tn A C B P *)
      assert(Per P B A).
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
        apply(l11_18_2 P B A C); auto.
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
        apply conga_comm.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
        assumption.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
      eapply (col_per_perp _ _ _ C) in H12; auto.
(* Goal: @Perp Tn A C B P *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
        apply perp_right_comm.
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
        assumption.
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
      apply bet_col in H11.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
      Col.
(* Goal: @Perp Tn A C B P *)
    assert(B <> T).
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
      intro.
(* Goal: False *)
(* Goal: @Col Tn T A C *)
      subst T.
(* Goal: False *)
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
      contradiction.
(* Goal: @Perp Tn A C B P *)
    assert(CongA T B A T B C).
(* Goal: or (@Bet Tn B P T) (@Bet Tn B T P) *)
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
      induction H5.
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
        eapply (l11_13 P _ _ P); Between.
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
        apply conga_comm.
(* Goal: @CongA Tn A B P C B P *)
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
        apply H1.
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
      assert(Out B P T).
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
        repeat split; auto.
(* Goal: or (@Bet Tn B P T) (@Bet Tn B T P) *)
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
        induction H5.
(* Goal: or (@Bet Tn B P T) (@Bet Tn B T P) *)
(* Goal: or (@Bet Tn B P T) (@Bet Tn B T P) *)
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
          left.
(* Goal: @Bet Tn B T P *)
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
          Between.
(* Goal: or (@Bet Tn B P T) (@Bet Tn B T P) *)
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
        right.
(* Goal: @Bet Tn B T P *)
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
        Between.
(* Goal: @CongA Tn T B A T B C *)
(* Goal: @Perp Tn A C B P *)
      apply conga_comm.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
      eapply (out_conga A _ P C _ P); auto.
(* Goal: @Out Tn B C C *)
(* Goal: @Perp Tn A C B P *)
        apply out_trivial.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
        auto.
(* Goal: @Out Tn B C C *)
(* Goal: @Perp Tn A C B P *)
      apply out_trivial.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
      auto.
(* Goal: @Perp Tn A C B P *)
    assert(Cong T A T C).
      apply (cong2_conga_cong T B A T B C); Cong.
(* Goal: @Perp Tn A C B P *)
    assert(Midpoint T A C).
      split; Cong.
(* Goal: @Perp Tn A C B P *)
    assert(Per B T A).
(* Goal: @Per Tn B T A *)
(* Goal: @Perp Tn A C B P *)
      unfold Per.
(* Goal: @ex (@Tpoint Tn) (fun C' : @Tpoint Tn => and (@Midpoint Tn T A C') (@Cong Tn B A B C')) *)
(* Goal: @Perp Tn A C B P *)
      exists C.
      split; Cong.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
    eapply (col_per_perp _ _ _ C) in H16; auto.
(* Goal: @Perp Tn A C B P *)
(* Goal: not (@eq (@Tpoint Tn) T A) *)
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
      apply perp_sym.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
      apply (perp_col _ T); Col.
(* Goal: @Perp Tn B T A C *)
(* Goal: not (@eq (@Tpoint Tn) T A) *)
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
      Perp.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
      intro.
(* Goal: False *)
(* Goal: @Col Tn T A C *)
      subst T.
(* Goal: False *)
(* Goal: @Col Tn T A C *)
      apply is_midpoint_id in H15.
(* Goal: False *)
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
      contradiction.
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
      intro.
(* Goal: False *)
(* Goal: @Col Tn T A C *)
      subst T.
(* Goal: False *)
(* Goal: @Col Tn T A C *)
      apply l7_2 in H15.
(* Goal: False *)
(* Goal: @Col Tn T A C *)
      apply is_midpoint_id in H15.
(* Goal: False *)
(* Goal: @Col Tn T A C *)
      apply H10.
(* Goal: @eq (@Tpoint Tn) A C *)
(* Goal: @Col Tn T A C *)
      auto.
(* Goal: @Col Tn T A C *)
    apply bet_col in H6.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
    Col.
Qed.

Lemma perp_inter_exists : forall A B C D, Perp A B C D -> exists P, Col A B P /\ Col C D P.
Proof.
(* Goal: @Perp Tn B T A C *)
(* Goal: not (@eq (@Tpoint Tn) T A) *)
(* Goal: not (@eq (@Tpoint Tn) C T) *)
(* Goal: @Col Tn T A C *)
    intros A B C D HPerp.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn A B P) (@Col Tn C D P)) *)
    destruct HPerp as [P [_ [_ [HCol1 [HCol2]]]]].
(* Goal: and (@Col Tn P A B) (@Col Tn P X Y) *)
(* Goal: False *)
    exists P; split; Col.
Qed.

Lemma perp_inter_perp_in : forall A B C D, Perp A B C D -> exists P, Col A B P /\ Col C D P /\ Perp_at P A B C D.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
    intros.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn A B P) (and (@Col Tn C D P) (@Perp_at Tn P A B C D))) *)
    assert(HH:=perp_inter_exists A B C D H).
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn A B P) (and (@Col Tn C D P) (@Perp_at Tn P A B C D))) *)
    ex_and HH P.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn A B P) (and (@Col Tn C D P) (@Perp_at Tn P A B C D))) *)
    exists P.
(* Goal: and (@Col Tn C D P) (@Perp_at Tn P A B C D) *)
    split.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
      Col.
(* Goal: and (@Col Tn C D P) (@Perp_at Tn P A B C D) *)
    split.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
      Col.
(* Goal: @Col Tn C D P *)
(* Goal: @Perp_at Tn P A B C D *)
    apply l8_14_2_1b_bis; Col.
Qed.

End T12_3.

Section T12_2D.

(* Goal: @Acute Tn T B P' *)
(* Goal: @Perp Tn B P' T P *)
Context `{T2D:Tarski_2D}.

Lemma col_perp2__col : forall X1 X2 Y1 Y2 A B,
  Perp X1 X2 A B -> Perp Y1 Y2 A B -> Col X1 Y1 Y2 -> Col X2 Y1 Y2.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
  intros.
(* Goal: @Col Tn X2 Y1 Y2 *)
  apply col_cop2_perp2__col with X1 A B; trivial; apply all_coplanar.
Qed.

Lemma l12_9_2D : forall A1 A2 B1 B2 C1 C2,
  Perp A1 A2 C1 C2 -> Perp B1 B2 C1 C2 -> Par A1 A2 B1 B2.
Proof.
(* Goal: forall (A1 A2 B1 B2 C1 C2 : @Tpoint Tn) (_ : @Perp Tn A1 A2 C1 C2) (_ : @Perp Tn B1 B2 C1 C2), @Par Tn A1 A2 B1 B2 *)
  intros A1 A2 B1 B2 C1 C2.
(* Goal: forall (_ : @Perp Tn A1 A2 C1 C2) (_ : @Perp Tn B1 B2 C1 C2), @Par Tn A1 A2 B1 B2 *)
  apply l12_9; apply all_coplanar.
Qed.

Lemma conga_inangle_per2__inangle : forall A B C P T,
  Per A B C -> InAngle T A B C -> CongA P B A P B C -> Per B P T ->
  InAngle P A B C.
Proof.
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : @CongA Tn P B A P B C) (_ : @Per Tn B P T), @InAngle Tn P A B C *)
  intros.
(* Goal: @InAngle Tn P A B C *)
  assert (HCop := all_coplanar A B C P).
(* Goal: @Perp Tn A C P B *)
(* Goal: @Col Tn B A C *)
(* Goal: @Perp Tn A C B P *)
  apply conga_cop_inangle_per2__inangle with T; assumption.
Qed.

End T12_2D.