Require Export GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates.
Require Export GeoCoq.Meta_theory.Parallel_postulates.par_trans_NID.

Section T13.

Context `{TE:Tarski_euclidean}.

Lemma cop_npar__inter_exists : forall A1 B1 A2 B2,
  Coplanar A1 B1 A2 B2 -> ~ Par A1 B1 A2 B2 -> exists X, Col X A1 B1 /\ Col X A2 B2.
Proof.
(* Goal: forall (A B A' B' X Y : @Tpoint Tn) (_ : not (@Par Tn A B A' B')), @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B'))) *)
intros.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A1 B1) (@Col Tn X A2 B2)) *)
induction (eq_dec_points A1 B1).
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A1 B1) (@Col Tn X A2 B2)) *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A1 B1) (@Col Tn X A2 B2)) *)
subst; exists A2; Col.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A1 B1) (@Col Tn X A2 B2)) *)
induction (eq_dec_points A2 B2).
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A1 B1) (@Col Tn X A2 B2)) *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A1 B1) (@Col Tn X A2 B2)) *)
subst; exists A1; Col.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A1 B1) (@Col Tn X A2 B2)) *)
induction (inter_dec A1 B1 A2 B2).

(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
  assumption.

(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A1 B1) (@Col Tn X A2 B2)) *)
  exfalso.
(* Goal: False *)
  apply H0.
(* Goal: @Par Tn A1 B1 A2 B2 *)
  unfold Par.
(* Goal: or (not (@Par Tn A B X Y)) (not (@Par Tn A' B' X Y)) *)
  left.
(* Goal: @Par_strict Tn A1 B1 A2 B2 *)
  unfold Par_strict.
(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
  repeat split; assumption.
Qed.

Lemma cop_npar__inter : forall A1 B1 A2 B2, A1 <> B1 -> A2 <> B2 ->
  Coplanar A1 B1 A2 B2 -> ~ Par A1 B1 A2 B2 -> exists X, Inter A1 B1 A2 B2 X.
Proof.
(* Goal: forall (A B A' B' X Y : @Tpoint Tn) (_ : not (@Par Tn A B A' B')), @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B'))) *)
intros.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Inter Tn A1 B1 A2 B2 X) *)
destruct (cop_npar__inter_exists A1 B1 A2 B2) as [X []].
(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
  assumption.
(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
  assumption.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @Inter Tn A1 B1 A2 B2 X) *)
exists X.
(* Goal: and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B')) *)
split.
(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
  assumption.
(* Goal: and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B')) *)
split.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn P A2 B2) (not (@Col Tn P A1 B1))) *)
(* Goal: and (@Col Tn A1 B1 X) (@Col Tn A2 B2 X) *)
  induction (col_dec A2 A1 B1).
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn P A2 B2) (not (@Col Tn P A1 B1))) *)
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn P A2 B2) (not (@Col Tn P A1 B1))) *)
(* Goal: and (@Col Tn A1 B1 X) (@Col Tn A2 B2 X) *)
    exists B2.
(* Goal: and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B')) *)
    split.
(* Goal: @Col Tn A' B' C' *)
      Col.
(* Goal: not (@Par Tn A' B' X Y) *)
(* Goal: or (not (@Par Tn A B X Y)) (not (@Par Tn A' B' X Y)) *)
    intro.
(* Goal: False *)
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn P A2 B2) (not (@Col Tn P A1 B1))) *)
(* Goal: and (@Col Tn A1 B1 X) (@Col Tn A2 B2 X) *)
    apply H2.
(* Goal: @Par Tn A B B C *)
(* Goal: @Col Tn A' B' C' *)
    right.
(* Goal: and (not (@eq (@Tpoint Tn) A1 B1)) (and (not (@eq (@Tpoint Tn) A2 B2)) (and (@Col Tn A1 A2 B2) (@Col Tn B1 A2 B2))) *)
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn P A2 B2) (not (@Col Tn P A1 B1))) *)
(* Goal: and (@Col Tn A1 B1 X) (@Col Tn A2 B2 X) *)
    repeat split; ColR.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X B1 B1) (@Col Tn X A2 B2)) *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A1 B1) (@Col Tn X A2 B2)) *)
  exists A2.
(* Goal: @Col Tn A' B' C' *)
  split; Col.
(* Goal: @Col Tn A' B' C' *)
split; Col.
Qed.

Lemma parallel_uniqueness :
 forall A1 A2 B1 B2 C1 C2 P : Tpoint,
  Par A1 A2 B1 B2 -> Col P B1 B2 ->
  Par A1 A2 C1 C2 -> Col P C1 C2 ->
  Col C1 B1 B2 /\ Col C2 B1 B2.
Proof.
(* Goal: forall (A1 A2 B1 B2 C1 C2 P : @Tpoint Tn) (_ : @Par Tn A1 A2 B1 B2) (_ : @Col Tn P B1 B2) (_ : @Par Tn A1 A2 C1 C2) (_ : @Col Tn P C1 C2), and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
    apply tarski_s_euclid_implies_playfair.
(* Goal: @tarski_s_parallel_postulate Tn *)
    unfold tarski_s_parallel_postulate; apply euclid.
Qed.

Lemma par_trans : forall A1 A2 B1 B2 C1 C2,
  Par A1 A2 B1 B2 -> Par B1 B2 C1 C2 -> Par A1 A2 C1 C2.
Proof.
(* Goal: forall (A B A' B' X Y : @Tpoint Tn) (_ : not (@Par Tn A B A' B')), @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B'))) *)
    intros.
(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
    apply playfair_implies_par_trans with B1 B2; [|assumption..].
(* Goal: @playfair_s_postulate Tn *)
    unfold playfair_s_postulate.
(* Goal: forall (A1 A2 B1 B2 C1 C2 P : @Tpoint Tn) (_ : @Par Tn A1 A2 B1 B2) (_ : @Col Tn P B1 B2) (_ : @Par Tn A1 A2 C1 C2) (_ : @Col Tn P C1 C2), and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
    apply parallel_uniqueness.
Qed.

Lemma inter__npar : forall A1 A2 B1 B2 X,
  Inter A1 A2 B1 B2 X -> ~ Par A1 A2 B1 B2.
Proof.
(* Goal: forall (A B A' B' X Y : @Tpoint Tn) (_ : not (@Par Tn A B A' B')), @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B'))) *)
    intros.
(* Goal: not (@Par Tn A1 A2 B1 B2) *)
    destruct H as [HA [[P []] []]].
(* Goal: not (@Par Tn A1 A2 B1 B2) *)
    induction 1.
(* Goal: @Col Tn A' B' C' *)
    apply (par_not_col A1 A2 B1 B2 X); Col.
(* Goal: @Col Tn A' B' C' *)
    spliter.
(* Goal: @Col Tn A' B' C' *)
    apply H0, (col3 B1 B2); Col.
Qed.

Lemma l12_16 : forall A1 A2 B1 B2 C1 C2 X,
  Par A1 A2 B1 B2 -> Coplanar B1 B2 C1 C2 -> Inter A1 A2 C1 C2 X -> exists Y, Inter B1 B2 C1 C2 Y.
Proof.
(* Goal: forall (A B A' B' X Y : @Tpoint Tn) (_ : not (@Par Tn A B A' B')), @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B'))) *)
    intros.
(* Goal: @CongA Tn B A P D C P *)
    assert_diffs.
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => @Inter Tn B1 B2 C1 C2 Y) *)
    apply cop_npar__inter; auto.
(* Goal: not (@eq (@Tpoint Tn) C1 C2) *)
(* Goal: not (@Par Tn B1 B2 C1 C2) *)
      destruct H1.
(* Goal: not (@eq (@Tpoint Tn) C1 C2) *)
(* Goal: not (@Par Tn B1 B2 C1 C2) *)
      auto.
(* Goal: not (@Par Tn A' B' X Y) *)
(* Goal: or (not (@Par Tn A B X Y)) (not (@Par Tn A' B' X Y)) *)
    intro.
(* Goal: False *)
    apply inter__npar in H1.
(* Goal: False *)
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B'))) *)
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B'))) *)
    apply H1.
(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
    apply par_trans with B1 B2; assumption.
Qed.

Lemma par_dec : forall A B C D, Par A B C D \/ ~ Par A B C D.
Proof. exact (par_trans__par_dec par_trans). Qed.

Lemma par_not_par : forall A B C D P Q, Par A B C D -> ~Par A B P Q -> ~Par C D P Q.
Proof.
(* Goal: forall (A B C D P Q : @Tpoint Tn) (_ : @Par Tn A B C D) (_ : not (@Par Tn A B P Q)), not (@Par Tn C D P Q) *)
intros A B C D P Q HPar HNPar.
(* Goal: not (@Par Tn C D P Q) *)
intro HNPar'.
(* Goal: False *)
apply HNPar.
(* Goal: @Par Tn A B P Q *)
apply par_trans with C D; Par.
Qed.

Lemma cop_par__inter : forall A B C D P Q,
  Par A B C D -> ~Par A B P Q -> Coplanar C D P Q ->
  exists Y, Col P Q Y /\ Col C D Y.
Proof.
(* Goal: forall (A B C D P Q : @Tpoint Tn) (_ : @Par Tn A B C D) (_ : not (@Par Tn A B P Q)) (_ : @Coplanar Tn C D P Q), @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Col Tn P Q Y) (@Col Tn C D Y)) *)
    intros A B C D P Q HPar HNPar HCop.
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Col Tn P Q Y) (@Col Tn C D Y)) *)
    destruct (cop_npar__inter_exists C D P Q) as [Y []].
(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
      assumption.
(* Goal: not (@Par Tn A' B' X Y) *)
(* Goal: or (not (@Par Tn A B X Y)) (not (@Par Tn A' B' X Y)) *)
      intro.
(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
      apply HNPar, par_trans with C D; assumption.
(* Goal: @Col Tn A' B' C' *)
    exists Y; split; Col.
Qed.

Lemma l12_19 :
  forall A B C D ,
   ~Col A B C -> Par A B C D -> Par B C D A ->
   Cong A B C D /\ Cong B C D A /\ TS B D A C /\ TS A C B D.
Proof.
(* Goal: forall (A B A' B' X Y : @Tpoint Tn) (_ : not (@Par Tn A B A' B')), @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B'))) *)
    intros.
    assert(exists P, Midpoint P A C) by (eapply midpoint_existence).
    ex_and H2 P.
    double B P D'.
    assert(Cong C D' A B).
(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
      apply (l7_13 P); assumption.
    assert(Cong B C D' A).
      apply (l7_13 P); Midpoint.
    assert(Par A B C D').
(* Goal: not (@eq (@Tpoint Tn) C1 C2) *)
(* Goal: not (@Par Tn B1 B2 C1 C2) *)
      assert_diffs; apply l12_17 with P; auto.
    assert(Par C D C D').
      eapply par_trans.
        apply par_symmetry.
(* Goal: False *)
        apply H0.
      apply H6.
    assert(Col C D D').
      apply par_id.
(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
      assumption.
    assert(Par B C D' A).
      assert_diffs; apply l12_17 with P; Midpoint.
    assert(Par D A D' A).
      eapply par_trans.
        apply par_symmetry.
(* Goal: False *)
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B'))) *)
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B'))) *)
        apply H1.
(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
      assumption.
    assert(Col A D D').
      apply par_id.
(* Goal: @Par Tn B C B' C' *)
(* Goal: @Col Tn A' B' C' *)
      Par.
    assert(D = D').
(* Goal: @Col Tn A' B' C' *)
      assert_diffs; apply (l6_21 A D C D); Col.
(* Goal: not (@Par Tn A' B' X Y) *)
(* Goal: or (not (@Par Tn A B X Y)) (not (@Par Tn A' B' X Y)) *)
        intro.
(* Goal: False *)
(* Goal: or (not (@Par Tn A B X Y)) (not (@Par Tn A' B' X Y)) *)
        apply H.
        assert(Col P C D).
          apply col_permutation_2.
(* Goal: @Col Tn A' B' C' *)
          apply (col_transitivity_1 _ A); Col.
        assert(Col P C D').
          apply col_permutation_2.
(* Goal: @Col Tn A' B' C' *)
          apply (col_transitivity_1 _ D); Col.
        assert(Col P A D').
(* Goal: @Col Tn A' B' C' *)
          apply (col_transitivity_1 _ C); Col.
(* Goal: @Col Tn A' B' C' *)
        apply (col3 P D'); Col.
(* Goal: @Col Tn A' B' C' *)
        intro; treat_equalities; assert_cols; Col.
    subst D'.
(* Goal: and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B')) *)
    split.
      Cong.
(* Goal: and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B')) *)
    split.
      Cong.
    assert(B <> D).
(* Goal: @Col Tn A' B' C' *)
      intro; treat_equalities; assert_cols; Col.
(* Goal: and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B')) *)
    split.
(* Goal: @Col Tn A' B' C' *)
      apply l12_18_c with P; Cong; Col.
(* Goal: @Col Tn A' B' C' *)
    apply l12_18_d with P; Cong; Col.
Qed.

Lemma l12_20_bis :
  forall A B C D,
   Par A B C D -> Cong A B C D -> TS B D A C ->
   Par B C D A /\ Cong B C D A /\ TS A C B D.
Proof.
(* Goal: forall (A B A' B' X Y : @Tpoint Tn) (_ : not (@Par Tn A B A' B')), @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B'))) *)
    intros.
    assert(B <> C) by (assert_diffs; auto).
    assert(A <> D) by (assert_diffs; auto).
    assert(~ Col A B C).
(* Goal: not (@Par Tn A' B' X Y) *)
(* Goal: or (not (@Par Tn A B X Y)) (not (@Par Tn A' B' X Y)) *)
      intro.
      assert(Col A B D).
(* Goal: @Par Tn B C B' C' *)
(* Goal: @Col Tn A' B' C' *)
        apply not_strict_par1 with C C; Col; Par.
      unfold TS in H1.
(* Goal: @Col Tn A' B' C' *)
      spliter.
      contradiction.
    assert(exists P, Midpoint P A C) by (apply midpoint_existence).
    ex_and H5 P.
    double B P D'.
    assert(Par B C D' A).
      eapply l12_17.
(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
        assumption.
        apply H5.
      apply l7_2.
(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
      assumption.
    assert(Par A B C D').
(* Goal: not (@eq (@Tpoint Tn) C1 C2) *)
(* Goal: not (@Par Tn B1 B2 C1 C2) *)
      assert_diffs; apply l12_17 with P; auto.
    assert(Cong C D' A B).
(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
      apply (l7_13 P); assumption.
    assert(Cong B C D' A).
      apply (l7_13 P); Midpoint.
    assert(Par C D C D').
      eapply par_trans.
        apply par_symmetry.
(* Goal: False *)
(* Goal: or (not (@Par Tn A B X Y)) (not (@Par Tn A' B' X Y)) *)
        apply H.
(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
      assumption.
    assert(Col C D D').
(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
      apply par_id; assumption.
    assert(Cong C D C D').
      apply (cong_transitivity _ _ A B); Cong.
    assert(D = D' \/ Midpoint C D D').
(* Goal: @Col Tn A' B' C' *)
      apply l7_20; Col.
    induction H14.
    { subst D'.
(* Goal: @Par Tn B C B' C' *)
(* Goal: @Col Tn A' B' C' *)
      assert(Par B C D A) by Par.
(* Goal: and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B')) *)
      split.
(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
        assumption.
      assert(HH:=l12_19 A B C D H4 H H14).
(* Goal: @Col Tn A' B' C' *)
      spliter.
(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
      split; assumption.
    }
    (************)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A1 B1) (@Col Tn X A2 B2)) *)
    exfalso.
    assert(TS A C B D).
(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
      apply par_two_sides_two_sides; assumption.
    assert(~ Col A C D).
(* Goal: @Col Tn A' B' C' *)
      apply (par_not_col A B C D A); Col.
(* Goal: @Col Tn A' B' C' *)
      apply par_not_col_strict with C; Col.
    assert(~ Col D' A C).
(* Goal: not (@Par Tn A' B' X Y) *)
(* Goal: or (not (@Par Tn A B X Y)) (not (@Par Tn A' B' X Y)) *)
      intro.
      apply H16.
      ColR.
    assert(TS A C B D').
(* Goal: @Col Tn A' B' C' *)
      repeat split; Col.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B'))) *)
      exists P.
(* Goal: and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B')) *)
      split.
(* Goal: @Col Tn A' B' C' *)
        Col.
      Between.
    assert (TS A C D D').
(* Goal: @Col Tn A' B' C' *)
      repeat split; Col.
      exists C.
(* Goal: and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B')) *)
      split.
(* Goal: @Col Tn A' B' C' *)
        Col.
      Between.
    apply (l9_9 A C B D).
(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
      assumption.
(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
    apply l9_8_1 with D'; assumption.
Qed.

Lemma l12_20 :
 forall A B C D,
  Par A B C D -> Cong A B C D -> TS A C B D ->
  Par B C D A /\ Cong B C D A /\ TS A C B D.
Proof.
(* Goal: forall (A B A' B' X Y : @Tpoint Tn) (_ : not (@Par Tn A B A' B')), @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B'))) *)
    intros.
(* Goal: and (@Par Tn B C D A) (and (@Cong Tn B C D A) (@TS Tn A C B D)) *)
    assert(TS B D A C).
(* Goal: @TS Tn B D A C *)
(* Goal: and (@Par Tn B C D A) (and (@Cong Tn B C D A) (@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: and (@Par Tn B C D A) (and (@Cong Tn B C D A) (@TS Tn A C B D)) *)
        apply par_comm.
(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
        assumption.
(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
      assumption.
(* Goal: and (@Par Tn B C D A) (and (@Cong Tn B C D A) (@TS Tn A C B D)) *)
    assert(HH:=l12_20_bis A B C D H H0 H2).
(* Goal: @Col Tn A' B' C' *)
    spliter.
(* Goal: and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B')) *)
    split.
(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
      assumption.
(* Goal: and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B')) *)
    split.
(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
      assumption.
(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
    assumption.
Qed.

Lemma l12_21_a :
 forall A B C D,
  TS A C B D ->
  (Par A B C D -> CongA B A C D C A).
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @TS Tn A C B D) (_ : @Par Tn A B C D), @CongA Tn B A C D C A *)
    apply postulates_in_euclidean_context; simpl; repeat (try (left; reflexivity); right).
Qed.

Lemma l12_21 : 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 A' B' X Y : @Tpoint Tn) (_ : not (@Par Tn A B A' B')), @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B'))) *)
    intros.
(* Goal: and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B')) *)
    split.
(* Goal: not (@Par Tn A' B' X Y) *)
(* Goal: or (not (@Par Tn A B X Y)) (not (@Par Tn A' B' X Y)) *)
      intro.
(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
      apply l12_21_b ; assumption.
(* Goal: not (@Par Tn A' B' X Y) *)
(* Goal: or (not (@Par Tn A B X Y)) (not (@Par Tn A' B' X Y)) *)
    intro.
(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
    apply l12_21_a; assumption.
Qed.

Lemma l12_22_a : forall A B C D P,
 Out P A C -> OS P A B D -> Par A B C D ->
 CongA B A P D C P.
Proof.
    cut (forall A B C D P,
         A <> P -> Bet P A C -> OS P A B D -> Par A B C D ->
         CongA B A P D C P).
(* Goal: @Par Tn B C B' C' *)
(* Goal: @Col Tn A' B' C' *)
    { intros Haux A B C D P HOut HOS HPar.
(* Goal: @CongA Tn B A P D C P *)
      destruct HOut as [HAP [HCP [|]]].
(* Goal: @CongA Tn B A P D C P *)
(* Goal: @CongA Tn B A P D C P *)
        apply Haux; trivial.
(* Goal: @Par Tn B C B' C' *)
(* Goal: @Col Tn A' B' C' *)
      apply conga_sym, Haux; Par.
(* Goal: @OS Tn P C D B *)
      apply col_one_side with A; Col; Side.
    }
(* Goal: @Par Tn B C B' C' *)
(* Goal: @Col Tn A' B' C' *)
    intros A B C D P HAP HBet HOS HPar.
(* Goal: @CongA Tn B A P D C P *)
    destruct (eq_dec_points A C).
(* Goal: @CongA Tn B A P D C P *)
(* Goal: @CongA Tn B A P D C P *)
    { subst C.
(* Goal: @CongA Tn B A P D A P *)
      apply out2__conga; [|apply out_trivial; auto].
(* Goal: @Out Tn A D B *)
      apply col_one_side_out with P; Side.
(* Goal: @Par Tn B C B' C' *)
(* Goal: @Col Tn A' B' C' *)
      apply par_id; Par.
    }
(* Goal: @CongA Tn B A P D C P *)
    destruct (segment_construction B A B A) as [B' []].
(* Goal: @CongA Tn B A P D C P *)
    assert_diffs.
(* Goal: @CongA Tn B A P D C P *)
    apply conga_trans with B' A C.
(* Goal: not (@eq (@Tpoint Tn) C1 C2) *)
(* Goal: not (@Par Tn B1 B2 C1 C2) *)
      apply l11_14; auto.
(* Goal: @CongA Tn B' A C D C P *)
    apply l11_10 with B' C D A; try (apply out_trivial); auto; [|apply l6_6, bet_out; Between].
(* Goal: @CongA Tn B' A C D C A *)
    apply l12_21_a; [|apply par_col_par_2 with B; Col].
(* Goal: @TS Tn A C B' D *)
    apply l9_2, l9_8_2 with B; [|apply col_one_side with P; Side; Col].
(* Goal: @TS Tn A C B B' *)
    assert (HNCol : ~ Col P A B) by (apply one_side_not_col123 with D, HOS).
(* Goal: @TS Tn A C B B' *)
    assert (HNCol1 : ~ Col B A C) by (intro; apply HNCol; ColR).
(* Goal: @TS Tn A C B B' *)
    repeat split; trivial.
      intro; apply HNCol1; ColR.
(* Goal: @Col Tn A' B' C' *)
    exists A; Col.
Qed.

Lemma l12_22 :
  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 A' B' X Y : @Tpoint Tn) (_ : not (@Par Tn A B A' B')), @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B'))) *)
    intros.
(* Goal: not (@Par Tn A' B' X Y) *)
(* Goal: or (not (@Par Tn A B X Y)) (not (@Par Tn A' B' X Y)) *)
    split; intro.
(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
      apply (l12_22_b _ _ _ _ P); assumption.
(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
      apply l12_22_a; assumption.
Qed.

Lemma l12_23 :
 forall A B C,
  ~Col A B C ->
  exists B', exists C',
  TS A C B B' /\ TS A B C C' /\
      Bet B' A C' /\ CongA A B C B A C' /\ CongA A C B C A B'.
Proof.
(* Goal: forall (A B A' B' X Y : @Tpoint Tn) (_ : not (@Par Tn A B A' B')), @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B'))) *)
    intros.
    assert(exists B0, Midpoint B0 A B) by (apply midpoint_existence).
    assert(exists C0, Midpoint C0 A C) by (apply midpoint_existence).
    ex_and H0 B0.
    ex_and H1 C0.
    prolong B C0 B' B C0.
    prolong C B0 C' C B0.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A' B') (@Col Tn X B' C')) *)
(* Goal: @Col Tn A' B' C' *)
    exists B'.
    exists C'.
    assert(TS A C B B').
(* Goal: @Col Tn A' B' C' *)
      apply mid_two_sides with C0; Col.
(* Goal: and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B')) *)
      split.
(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
        assumption.
      Cong.
    assert(TS A B C C').
(* Goal: @Col Tn A' B' C' *)
      eapply mid_two_sides with B0; Col.
(* Goal: and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B')) *)
      split.
(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
        assumption.
      Cong.
(* Goal: and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B')) *)
    split.
(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
      assumption.
(* Goal: and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B')) *)
    split.
(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
      assumption.
    assert(Par A B' C B).
      eapply l12_17.
(* Goal: not (@Par Tn A' B' X Y) *)
(* Goal: or (not (@Par Tn A B X Y)) (not (@Par Tn A' B' X Y)) *)
        intro.
        treat_equalities.
        assert(C0 = B0).
          eapply l7_17.
(* Goal: False *)
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn P A2 B2) (not (@Col Tn P A1 B1))) *)
(* Goal: and (@Col Tn A1 B1 X) (@Col Tn A2 B2 X) *)
            2: apply H2.
(* Goal: and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B')) *)
          split.
            apply between_symmetry.
(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
            assumption.
          Cong.
        treat_equalities.
(* Goal: @Col Tn A' B' C' *)
        Col.
(* Goal: False *)
        apply H0.
(* Goal: and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B')) *)
      split.
        apply between_symmetry.
(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
        assumption.
      Cong.
    assert(Par A C' B C).
      eapply l12_17.
(* Goal: not (@Par Tn A' B' X Y) *)
(* Goal: or (not (@Par Tn A B X Y)) (not (@Par Tn A' B' X Y)) *)
        intro.
        treat_equalities.
        assert(C0 = B0).
          eapply l7_17.
(* Goal: False *)
            apply H0.
(* Goal: and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B')) *)
          split.
            apply between_symmetry.
(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
            assumption.
          Cong.
        treat_equalities.
(* Goal: @Col Tn A' B' C' *)
        Col.
(* Goal: False *)
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn P A2 B2) (not (@Col Tn P A1 B1))) *)
(* Goal: and (@Col Tn A1 B1 X) (@Col Tn A2 B2 X) *)
        apply H2.
(* Goal: and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B')) *)
      split.
        apply between_symmetry.
(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
        assumption.
      Cong.
    assert(Par A B' A C').
      eapply par_trans.
        apply H8.
      apply par_symmetry.
      apply par_right_comm.
(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
      assumption.
    apply par_id in H10.
    assert(OS A C B0 C').
      eapply out_one_side_1.
(* Goal: not (@Par Tn A' B' X Y) *)
(* Goal: or (not (@Par Tn A B X Y)) (not (@Par Tn A' B' X Y)) *)
        intro.
(* Goal: False *)
(* Goal: or (not (@Par Tn A B X Y)) (not (@Par Tn A' B' X Y)) *)
        apply H.
(* Goal: @CongA Tn B A P D C P *)
        assert_diffs.
(* Goal: @Col Tn A' B' C' *)
        eapply (col_transitivity_1 _ B0); Col.
        apply col_trivial_2.
      apply bet_out.
(* Goal: not (@Par Tn A' B' X Y) *)
(* Goal: or (not (@Par Tn A B X Y)) (not (@Par Tn A' B' X Y)) *)
        intro.
        treat_equalities.
(* Goal: not (@eq (@Tpoint Tn) C1 C2) *)
(* Goal: not (@Par Tn B1 B2 C1 C2) *)
        assert_diffs; auto.
(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
      assumption.
    assert(OS A C B0 B).
      eapply out_one_side_1.
(* Goal: not (@Par Tn A' B' X Y) *)
(* Goal: or (not (@Par Tn A B X Y)) (not (@Par Tn A' B' X Y)) *)
        intro.
(* Goal: False *)
(* Goal: or (not (@Par Tn A B X Y)) (not (@Par Tn A' B' X Y)) *)
        apply H.
(* Goal: @Col Tn A' B' C' *)
        eapply (col_transitivity_1 _ B0); Col.
(* Goal: not (@Par Tn A' B' X Y) *)
(* Goal: or (not (@Par Tn A B X Y)) (not (@Par Tn A' B' X Y)) *)
          intro.
          treat_equalities.
(* Goal: @Col Tn A' B' C' *)
          Col.
        apply col_trivial_3.
      assert_diffs; apply bet_out; Between.
    assert(OS A C B C').
      eapply one_side_transitivity.
        2:apply H11.
      apply one_side_symmetry.
(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
      assumption.
    assert(TS A C B' C').
      apply l9_2.
      eapply l9_8_2.
        apply H6.
(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
      assumption.
(* Goal: and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B')) *)
    split.
(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
      apply col_two_sides_bet with C; assumption.
(* Goal: and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B')) *)
    split.
      apply l9_2 in H7.
      assert(HH:= l12_21_a A C' B C H7 H9); CongA.
    apply par_symmetry in H8.
    apply invert_two_sides in H6.
    assert(HH:= l12_21_a C B A B' H6 H8); CongA.
Qed.

Lemma cop_npars__inter_exists :
 forall A1 B1 A2 B2,
  Coplanar A1 B1 A2 B2 -> ~ Par_strict A1 B1 A2 B2 ->
  exists X, Col X A1 B1 /\ Col X A2 B2.
Proof.
(* Goal: forall (A B A' B' X Y : @Tpoint Tn) (_ : not (@Par Tn A B A' B')), @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B'))) *)
    intros.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A1 B1) (@Col Tn X A2 B2)) *)
    induction (eq_dec_points A1 B1).
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A1 B1) (@Col Tn X A2 B2)) *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A1 B1) (@Col Tn X A2 B2)) *)
      subst.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X B1 B1) (@Col Tn X A2 B2)) *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A1 B1) (@Col Tn X A2 B2)) *)
      exists A2.
(* Goal: @Col Tn A' B' C' *)
      Col.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A1 B1) (@Col Tn X A2 B2)) *)
    induction (eq_dec_points A2 B2).
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A1 B1) (@Col Tn X A2 B2)) *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A1 B1) (@Col Tn X A2 B2)) *)
      subst.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A1 B1) (@Col Tn X B2 B2)) *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A1 B1) (@Col Tn X A2 B2)) *)
      exists A1.
(* Goal: @Col Tn A' B' C' *)
      Col.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A1 B1) (@Col Tn X A2 B2)) *)
    induction (inter_dec A1 B1 A2 B2).
(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
      assumption.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A1 B1) (@Col Tn X A2 B2)) *)
    exfalso.
(* Goal: False *)
    apply H0.
(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
    repeat split; assumption.
Qed.

Lemma cop2_npar__inter : forall A B A' B' X Y,
  Coplanar A B X Y -> Coplanar A' B' X Y -> ~ Par A B A' B' ->
  (exists P, Col P X Y /\ (Col P A B \/ Col P A' B')).
Proof.
(* Goal: forall (A B A' B' X Y : @Tpoint Tn) (_ : not (@Par Tn A B A' B')), @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B'))) *)
    intros.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B'))) *)
    induction(par_dec A B X Y).
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B'))) *)
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B'))) *)
      assert(~ Par A' B' X Y).
(* Goal: not (@Par Tn A' B' X Y) *)
(* Goal: or (not (@Par Tn A B X Y)) (not (@Par Tn A' B' X Y)) *)
        intro.
(* Goal: False *)
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B'))) *)
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B'))) *)
        apply H1.
(* Goal: @Par Tn B C B' C' *)
(* Goal: @Col Tn A' B' C' *)
        apply(par_trans _ _ X Y); Par.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B'))) *)
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B'))) *)
      destruct(cop_npar__inter_exists A' B' X Y) as [P []].
(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
        assumption.
(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
        assumption.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B'))) *)
      exists P.
(* Goal: and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B')) *)
      split.
(* Goal: @Col Tn A' B' C' *)
        Col.
(* Goal: @Par Tn A B B C *)
(* Goal: @Col Tn A' B' C' *)
      right.
(* Goal: @Col Tn A' B' C' *)
      Col.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B'))) *)
    destruct(cop_npar__inter_exists A B X Y) as [P []].
(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
      assumption.
(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
      assumption.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B'))) *)
    exists P.
(* Goal: and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B')) *)
    split.
(* Goal: @Col Tn A' B' C' *)
      Col.
(* Goal: or (not (@Par Tn A B X Y)) (not (@Par Tn A' B' X Y)) *)
    left.
(* Goal: @Col Tn A' B' C' *)
    Col.
Qed.

Lemma not_par_one_not_par : forall A B A' B' X Y, ~Par A B A' B' -> ~Par A B X Y \/ ~Par A' B' X Y.
Proof.
(* Goal: forall (A B A' B' X Y : @Tpoint Tn) (_ : not (@Par Tn A B A' B')), @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B'))) *)
    intros.
(* Goal: or (not (@Par Tn A B X Y)) (not (@Par Tn A' B' X Y)) *)
    destruct (par_dec A B X Y).
(* Goal: @Par Tn A B B C *)
(* Goal: @Col Tn A' B' C' *)
      right.
(* Goal: not (@Par Tn A' B' X Y) *)
(* Goal: or (not (@Par Tn A B X Y)) (not (@Par Tn A' B' X Y)) *)
      intro.
(* Goal: False *)
(* Goal: or (not (@Par Tn A B X Y)) (not (@Par Tn A' B' X Y)) *)
      apply H.
(* Goal: @Par Tn B C B' C' *)
(* Goal: @Col Tn A' B' C' *)
      apply par_trans with X Y; Par.
(* Goal: or (not (@Par Tn A B X Y)) (not (@Par Tn A' B' X Y)) *)
    left.
(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
    assumption.
Qed.

Lemma col_par_par_col : forall A B C A' B' C', Col A B C -> Par A B A' B' -> Par B C B' C' -> Col A' B' C'.
Proof.
(* Goal: forall (A B A' B' X Y : @Tpoint Tn) (_ : not (@Par Tn A B A' B')), @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B'))) *)
    intros.
(* Goal: @Col Tn A' B' C' *)
    apply par_distincts in H0.
(* Goal: @Col Tn A' B' C' *)
    apply par_distincts in H1.
(* Goal: @Col Tn A' B' C' *)
    spliter.
(* Goal: @Col Tn A' B' C' *)
    assert(Par A B B C).
(* Goal: @Par Tn A B B C *)
(* Goal: @Col Tn A' B' C' *)
      right.
(* Goal: @Col Tn A' B' C' *)
      repeat split; Col.
(* Goal: @Col Tn A' B' C' *)
    assert(Par A' B' B' C').
(* Goal: @Par Tn A' B' B' C' *)
(* Goal: @Col Tn A' B' C' *)
      apply (par_trans _ _ A' B').
(* Goal: @Par Tn B C B' C' *)
(* Goal: @Col Tn A' B' C' *)
        Par.
(* Goal: @Par Tn A' B' B' C' *)
(* Goal: @Col Tn A' B' C' *)
      apply (par_trans _ _ B C).
(* Goal: @Par Tn B C B' C' *)
(* Goal: @Col Tn A' B' C' *)
        apply (par_trans _ _ A B); Par.
(* Goal: @Par Tn B C B' C' *)
(* Goal: @Col Tn A' B' C' *)
      Par.
(* Goal: @Col Tn A' B' C' *)
    induction H7.
(* Goal: @Col Tn A' B' C' *)
(* Goal: @Col Tn A' B' C' *)
      apply False_ind.
(* Goal: False *)
(* Goal: @Col Tn A' B' C' *)
      apply H7.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A' B') (@Col Tn X B' C')) *)
(* Goal: @Col Tn A' B' C' *)
      exists B'.
(* Goal: @Col Tn A' B' C' *)
      split; Col.
(* Goal: @Col Tn A' B' C' *)
    spliter.
(* Goal: @Col Tn A' B' C' *)
    Col.
Qed.

Lemma cop_par_perp__perp : forall A B C D P Q, Par A B C D -> Perp A B P Q -> Coplanar C D P Q ->
  Perp C D P Q.
Proof.
(* Goal: forall (A B C D P Q : @Tpoint Tn) (_ : @Par Tn A B C D) (_ : @Perp Tn A B P Q) (_ : @Coplanar Tn C D P Q), @Perp Tn C D P Q *)
    apply universal_posidonius_postulate__perpendicular_transversal_postulate.
(* Goal: @universal_posidonius_postulate Tn *)
    apply playfair__universal_posidonius_postulate.
(* Goal: forall (A1 A2 B1 B2 C1 C2 P : @Tpoint Tn) (_ : @Par Tn A1 A2 B1 B2) (_ : @Col Tn P B1 B2) (_ : @Par Tn A1 A2 C1 C2) (_ : @Col Tn P C1 C2), and (@Col Tn C1 B1 B2) (@Col Tn C2 B1 B2) *)
    unfold playfair_s_postulate; apply parallel_uniqueness.
Qed.

Lemma cop4_par_perp2__par : forall A B C D E F G H,
  Par A B C D -> Perp A B E F -> Perp C D G H ->
  Coplanar A B E G -> Coplanar A B E H ->
  Coplanar A B F G -> Coplanar A B F H ->
  Par E F G H.
Proof.
(* Goal: forall (A B C D E F G H : @Tpoint Tn) (_ : @Par Tn A B C D) (_ : @Perp Tn A B E F) (_ : @Perp Tn C D G H) (_ : @Coplanar Tn A B E G) (_ : @Coplanar Tn A B E H) (_ : @Coplanar Tn A B F G) (_ : @Coplanar Tn A B F H), @Par Tn E F G H *)
    apply par_perp_perp_implies_par_perp_2_par.
(* Goal: forall (A B A' B' X Y : @Tpoint Tn) (_ : not (@Par Tn A B A' B')), @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B'))) *)
    intros A B; intros.
(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
    apply (cop_par_perp__perp A B); assumption.
Qed.

End T13.

Section T13_2D.

(* Goal: @CongA Tn B A P D C P *)
(* Goal: @CongA Tn B A P D C P *)
Context `{T2D:Tarski_2D}.
(* Goal: @CongA Tn B A P D C P *)
(* Goal: @CongA Tn B A P D C P *)
Context `{TE:@Tarski_euclidean Tn TnEQD}.

Lemma not_par_inter_exists : forall A1 B1 A2 B2,
  ~ Par A1 B1 A2 B2 -> exists X, Col X A1 B1 /\ Col X A2 B2.
Proof.
(* Goal: forall (A B A' B' X Y : @Tpoint Tn) (_ : not (@Par Tn A B A' B')), @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B'))) *)
intros.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A1 B1) (@Col Tn X A2 B2)) *)
apply cop_npar__inter_exists.
(* Goal: @Coplanar Tn A1 B1 A2 B2 *)
(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
apply all_coplanar.
(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
assumption.
Qed.

Lemma l12_16_2D : forall A1 A2 B1 B2 C1 C2 X,
  Par A1 A2 B1 B2 -> Inter A1 A2 C1 C2 X -> exists Y, Inter B1 B2 C1 C2 Y.
Proof.
(* Goal: forall (A B A' B' X Y : @Tpoint Tn) (_ : not (@Par Tn A B A' B')), @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B'))) *)
    intros.
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => @Inter Tn B1 B2 C1 C2 Y) *)
    assert (HC := all_coplanar B1 B2 C1 C2).
(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
    apply l12_16 with A1 A2 X; assumption.
Qed.

Lemma par_inter : forall A B C D P Q,
  Par A B C D -> ~Par A B P Q ->
  exists Y, Col P Q Y /\ Col C D Y.
Proof.
(* Goal: forall (A B A' B' X Y : @Tpoint Tn) (_ : not (@Par Tn A B A' B')), @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B'))) *)
    intros.
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Col Tn P Q Y) (@Col Tn C D Y)) *)
    assert (HC := all_coplanar C D P Q).
(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
    apply (cop_par__inter A B); assumption.
Qed.

Lemma not_par_strict_inter_exists :
 forall A1 B1 A2 B2,
  ~Par_strict A1 B1 A2 B2 ->
  exists X, Col X A1 B1 /\ Col X A2 B2.
Proof.
(* Goal: forall (A B A' B' X Y : @Tpoint Tn) (_ : not (@Par Tn A B A' B')), @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B'))) *)
    intros.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A1 B1) (@Col Tn X A2 B2)) *)
    apply (cop_npars__inter_exists).
(* Goal: @Coplanar Tn A1 B1 A2 B2 *)
(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
    apply all_coplanar.
(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
    assumption.
Qed.

Lemma not_par_inter : forall A B A' B' X Y, ~Par A B A' B' -> (exists P, Col P X Y /\ (Col P A B \/ Col P A' B')).
Proof.
(* Goal: forall (A B A' B' X Y : @Tpoint Tn) (_ : not (@Par Tn A B A' B')), @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B'))) *)
    intros.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B'))) *)
    assert (HC := all_coplanar).
(* Goal: not (@eq (@Tpoint Tn) C1 C2) *)
(* Goal: not (@Par Tn B1 B2 C1 C2) *)
    apply (cop2_npar__inter); auto.
Qed.

Lemma par_perp__perp : forall A B C D P Q, Par A B C D -> Perp A B P Q ->
  Perp C D P Q.
Proof.
(* Goal: forall (A B C D P Q : @Tpoint Tn) (_ : @Par Tn A B C D) (_ : @Perp Tn A B P Q), @Perp Tn C D P Q *)
intros A B C D P Q HPar HPer.
(* Goal: @Perp Tn C D P Q *)
assert (HCop := all_coplanar C D P Q).
(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
apply (cop_par_perp__perp A B); assumption.
Qed.

Lemma par_perp2__par : forall A B C D E F G H,
  Par A B C D -> Perp A B E F -> Perp C D G H ->
  Par E F G H.
Proof.
(* Goal: forall (A B A' B' X Y : @Tpoint Tn) (_ : not (@Par Tn A B A' B')), @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (@Col Tn P X Y) (or (@Col Tn P A B) (@Col Tn P A' B'))) *)
intros A B C D; intros.
(* Goal: not (@Par_strict Tn A1 B1 A2 B2) *)
apply (cop4_par_perp2__par A B C D); try (apply all_coplanar); assumption.
Qed.

End T13_2D.