Require Import GeoCoq.Axioms.parallel_postulates.
Require Import GeoCoq.Meta_theory.Parallel_postulates.rah_thales_postulate.
Require Import GeoCoq.Meta_theory.Parallel_postulates.thales_converse_postulate_weak_triangle_circumscription_principle.
Require Import GeoCoq.Meta_theory.Parallel_postulates.thales_postulate_thales_converse_postulate.
Require Import GeoCoq.Meta_theory.Parallel_postulates.weak_triangle_circumscription_principle_bachmann_s_lotschnittaxiom.
Require Import GeoCoq.Tarski_dev.Annexes.saccheri.
Require Import GeoCoq.Tarski_dev.Ch12_parallel.

Section universal_posidonius_postulate_perpendicular_transversal_postulate.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma universal_posidonius_postulate__perpendicular_transversal_postulate :
  universal_posidonius_postulate -> perpendicular_transversal_postulate.
Proof.
(* Goal: forall _ : @universal_posidonius_postulate Tn, @perpendicular_transversal_postulate Tn *)
intros HP A B C D P Q HPar HPerp1 HCop.
elim HPar; intro HParS; [|destruct HParS as [_ [_ [HC1 HC2]]]; assert_diffs;
                          apply perp_sym; apply perp_col0 with A B; Col; ColR].
assert (H := HPerp1); destruct H as [R HR];
apply perp_in_col in HR; destruct HR as [HC1 HC2].
(* Goal: @Perp Tn C D P Q *)
assert (HEF : exists E F, Col A B E /\ Col C D F /\ Perp A B E F /\ E <> R).
(* Goal: @Saccheri Tn E F S R *)
(* Goal: @Perp Tn C D P Q *)
  {
  destruct (l8_18_existence A B C) as [E1 [HC3 HPerp2]];
  [apply par_strict_not_col_1 with D; Par|].
  destruct (l8_18_existence A B D) as [E2 [HC4 HPerp3]];
  [apply par_strict_not_col_1 with C; Par|].
  elim (eq_dec_points E1 R); intro; treat_equalities;
  [|exists E1, C; repeat (split; Col; Perp)].
  elim (eq_dec_points E1 E2); intro; treat_equalities;
  [|exists E2, D; repeat (split; Col; Perp)].
  assert (HC4 : Col E1 C D)
    by (apply cop_perp2__col with A B; Perp; apply par__coplanar in HPar; Cop).
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => @ex (@Tpoint Tn) (fun F : @Tpoint Tn => and (@Col Tn A B E) (and (@Col Tn C D F) (and (@Perp Tn A B E F) (not (@eq (@Tpoint Tn) E E1)))))) *)
  destruct HParS as [_ [_ [_ HF]]]; exfalso; apply HF; exists E1; Col.
  }
(* Goal: @Perp Tn C D P Q *)
destruct HEF as [E [F [HC3 [HC4 [HPerp2 HD1]]]]].
assert (HGH : exists G H,
                Col A B G /\ Col C D H /\ Perp A B G H /\ E <> G /\ F <> H).
(* Goal: @Saccheri Tn E F S R *)
(* Goal: @Perp Tn C D P Q *)
  {
  destruct (l8_18_existence A B C) as [E1 [HC5 HPerp3]];
  [apply par_strict_not_col_1 with D; Par|].
  destruct (l8_18_existence A B D) as [E2 [HC6 HPerp4]];
  [apply par_strict_not_col_1 with C; Par|].
  elim (eq_dec_points E1 E); intro HD; treat_equalities;
  [|exists E1, C; repeat (split; Col; Perp); intro; treat_equalities; apply HD;
    apply l6_21 with A B F E; assert_diffs; Col;
    [elim (perp_not_col2 _ _ _ _ HPerp2); Col|
     apply cop_perp2__col with A B; Perp]]; Cop.
  elim (eq_dec_points E1 E2); intro HD'; treat_equalities;
  [assert (HC7 : Col E1 C D)
     by (apply cop_perp2__col with A B; Perp; apply par__coplanar in HPar; Cop);
   destruct HParS as [_ [_ [_ HF]]]; exfalso; apply HF; exists E1; Col|].
(* Goal: @ex (@Tpoint Tn) (fun G : @Tpoint Tn => @ex (@Tpoint Tn) (fun H : @Tpoint Tn => and (@Col Tn A B G) (and (@Col Tn C D H) (and (@Perp Tn A B G H) (and (not (@eq (@Tpoint Tn) E1 G)) (not (@eq (@Tpoint Tn) F H))))))) *)
  exists E2, D; repeat (split; Col; Perp); intro; treat_equalities; apply HD'.
  apply l6_21 with A B F E1; assert_diffs; Col;
  [elim (perp_not_col2 _ _ _ _ HPerp2); Col|apply cop_perp2__col with A B; Perp;
                                            apply par__coplanar in HPar; Cop].
  }
(* Goal: @Perp Tn C D P Q *)
destruct HGH as [G [H [HC5 [HC6 [HPerp3 [HD2 HD3]]]]]].
(* Goal: @Perp Tn C D P Q *)
assert (HSacc1 : Saccheri E F H G).
(* Goal: @Saccheri Tn E F S R *)
(* Goal: @Perp Tn C D P Q *)
  {
(* Goal: @Saccheri Tn E F S R *)
  split; [apply perp_per_1; apply perp_col0 with A B; Perp|].
(* Goal: and (@Per Tn E G H) (and (@Cong Tn E F H G) (@OS Tn E G F H)) *)
  split; [apply perp_per_1; apply perp_sym; apply perp_col0 with A B; Perp|].
(* Goal: and (@Cong Tn E F H G) (@OS Tn E G F H) *)
  split; [assert (Cong E F G H); Cong; apply HP with A B C D; Col|].
(* Goal: @OS Tn E G F H *)
  apply l12_6; apply par_strict_col2_par_strict with C D; Col.
  apply par_strict_symmetry;
  apply par_strict_col2_par_strict with A B; Col; Par.
  }
(* Goal: @Perp Tn C D P Q *)
destruct (midpoint_existence E G) as [M1 HMid1].
(* Goal: @Perp Tn C D P Q *)
destruct (midpoint_existence F H) as [M2 HMid2].
(* Goal: @Perp Tn C D P Q *)
assert (HLamb := mid2_sac__lam6521 _ _ _ _ _ _ HSacc1 HMid2 HMid1).
(* Goal: @Perp Tn C D P Q *)
assert (HSacc2 : Saccheri E F M2 M1).
(* Goal: @Saccheri Tn E F S R *)
(* Goal: @Perp Tn C D P Q *)
  {
(* Goal: and (@Per Tn E M1 M2) (and (@Cong Tn E F M2 M1) (@OS Tn E M1 F M2)) *)
  split; [unfold Lambert in *; spliter; Perp|].
(* Goal: and (@Per Tn E M1 M2) (and (@Cong Tn E F M2 M1) (@OS Tn E M1 F M2)) *)
  split; [unfold Lambert in *; spliter; Perp|].
(* Goal: and (@Cong Tn E F M2 M1) (@OS Tn E M1 F M2) *)
  assert (HCong : Cong E F M1 M2); [|split; Cong].
(* Goal: @Saccheri Tn E F S R *)
(* Goal: @Perp Tn C D P Q *)
    {
(* Goal: @Cong Tn E F M1 M2 *)
    apply HP with A B C D; Col; try solve [assert_diffs; assert_cols; ColR].
    apply perp_sym; apply perp_col0 with E M1;
    try solve [assert_diffs; assert_cols; Col; ColR].
(* Goal: @Perp Tn E M1 M1 M2 *)
    apply per_perp; unfold Lambert in *; spliter; Perp.
    }
  apply l12_6; apply par_strict_col2_par_strict with C D; Col;
  try solve [assert_diffs; assert_cols; Col; ColR].
  apply par_strict_symmetry;
  apply par_strict_col2_par_strict with A B; Col; Par;
  assert_diffs; assert_cols; Col; ColR.
  }
assert (HRAH : postulate_of_right_saccheri_quadrilaterals)
  by (apply per_sac__rah with M1 M2 F E; try apply sac_perm;
      unfold Lambert in *; spliter; auto).
assert (HP' : forall A1 A2 B1 B2 C1 C2 D1 D2 IAB IAC IBD,
        Perp A1 A2 B1 B2 -> Perp A1 A2 C1 C2 -> Perp B1 B2 D1 D2 ->
        Col A1 A2 IAB -> Col B1 B2 IAB ->
        Col A1 A2 IAC -> Col C1 C2 IAC ->
        Col B1 B2 IBD -> Col D1 D2 IBD ->
        Coplanar IAB IAC IBD C1 -> Coplanar IAB IAC IBD C2 ->
        Coplanar IAB IAC IBD D1 -> Coplanar IAB IAC IBD D2 ->
       ~ Col IAB IAC IBD ->
        exists I, Col C1 C2 I /\ Col D1 D2 I).
(* Goal: @Saccheri Tn E F S R *)
(* Goal: @Perp Tn C D P Q *)
  {
(* Goal: forall (A1 A2 B1 B2 C1 C2 D1 D2 IAB IAC IBD : @Tpoint Tn) (_ : @Perp Tn A1 A2 B1 B2) (_ : @Perp Tn A1 A2 C1 C2) (_ : @Perp Tn B1 B2 D1 D2) (_ : @Col Tn A1 A2 IAB) (_ : @Col Tn B1 B2 IAB) (_ : @Col Tn A1 A2 IAC) (_ : @Col Tn C1 C2 IAC) (_ : @Col Tn B1 B2 IBD) (_ : @Col Tn D1 D2 IBD) (_ : @Coplanar Tn IAB IAC IBD C1) (_ : @Coplanar Tn IAB IAC IBD C2) (_ : @Coplanar Tn IAB IAC IBD D1) (_ : @Coplanar Tn IAB IAC IBD D2) (_ : not (@Col Tn IAB IAC IBD)), @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
  cut bachmann_s_lotschnittaxiom.

(* Goal: @Saccheri Tn E F S R *)
(* Goal: @Perp Tn C D P Q *)
    {
(* Goal: forall (_ : @bachmann_s_lotschnittaxiom Tn) (A1 A2 B1 B2 C1 C2 D1 D2 IAB IAC IBD : @Tpoint Tn) (_ : @Perp Tn A1 A2 B1 B2) (_ : @Perp Tn A1 A2 C1 C2) (_ : @Perp Tn B1 B2 D1 D2) (_ : @Col Tn A1 A2 IAB) (_ : @Col Tn B1 B2 IAB) (_ : @Col Tn A1 A2 IAC) (_ : @Col Tn C1 C2 IAC) (_ : @Col Tn B1 B2 IBD) (_ : @Col Tn D1 D2 IBD) (_ : @Coplanar Tn IAB IAC IBD C1) (_ : @Coplanar Tn IAB IAC IBD C2) (_ : @Coplanar Tn IAB IAC IBD D1) (_ : @Coplanar Tn IAB IAC IBD D2) (_ : not (@Col Tn IAB IAC IBD)), @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
    clear HP; clear dependent P; clear dependent Q; clear dependent R.
(* Goal: forall (_ : @bachmann_s_lotschnittaxiom Tn) (A1 A2 B1 B2 C1 C2 D1 D2 IAB IAC IBD : @Tpoint Tn) (_ : @Perp Tn A1 A2 B1 B2) (_ : @Perp Tn A1 A2 C1 C2) (_ : @Perp Tn B1 B2 D1 D2) (_ : @Col Tn A1 A2 IAB) (_ : @Col Tn B1 B2 IAB) (_ : @Col Tn A1 A2 IAC) (_ : @Col Tn C1 C2 IAC) (_ : @Col Tn B1 B2 IBD) (_ : @Col Tn D1 D2 IBD) (_ : @Coplanar Tn IAB IAC IBD C1) (_ : @Coplanar Tn IAB IAC IBD C2) (_ : @Coplanar Tn IAB IAC IBD D1) (_ : @Coplanar Tn IAB IAC IBD D2) (_ : not (@Col Tn IAB IAC IBD)), @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
    intros bla A1 A2 B1 B2 C1 C2 D1 D2 IAB IAC IBD HPerpAB HPerpAC HPerpBD.
(* Goal: forall (_ : @Col Tn A1 A2 IAB) (_ : @Col Tn B1 B2 IAB) (_ : @Col Tn A1 A2 IAC) (_ : @Col Tn C1 C2 IAC) (_ : @Col Tn B1 B2 IBD) (_ : @Col Tn D1 D2 IBD) (_ : @Coplanar Tn IAB IAC IBD C1) (_ : @Coplanar Tn IAB IAC IBD C2) (_ : @Coplanar Tn IAB IAC IBD D1) (_ : @Coplanar Tn IAB IAC IBD D2) (_ : not (@Col Tn IAB IAC IBD)), @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
    intros HCol1 HCol2 HCol3 HCol4 HCol5 HCol6 HCop1 HCop2 HCop3 HCop4 HNC1.
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
    assert (Col IAB IAC A1) by (assert_diffs; ColR).
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
    assert (Col IAB IAC A2) by (assert_diffs; ColR).
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
    assert (Col IAB IBD B1) by (assert_diffs; ColR).
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
    assert (Col IAB IBD B2) by (assert_diffs; ColR).
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
    assert (Coplanar IAB IAC IBD A1) by Cop.
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
    assert (Coplanar IAB IAC IBD A2) by Cop.
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
    assert (Coplanar IAB IAC IBD B1) by Cop.
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
    assert (Coplanar IAB IAC IBD B2) by Cop.
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
    assert (HNC2 : ~ Col A1 A2 D1).
(* Goal: @Saccheri Tn E F S R *)
(* Goal: @Perp Tn C D P Q *)
      {
      apply par_strict_not_col_1 with D2; apply par_not_col_strict with IBD;
      Col; try (intro; apply HNC1; assert_diffs; ColR).
(* Goal: @Par Tn A1 A2 D1 D2 *)
      apply l12_9 with B1 B2; Perp; CopR.
      }
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
    assert (HNC3 : ~ Col B1 B2 C1).
(* Goal: @Saccheri Tn E F S R *)
(* Goal: @Perp Tn C D P Q *)
      {
      apply par_strict_not_col_1 with C2; apply par_not_col_strict with IAC;
      Col; try (intro; apply HNC1; assert_diffs; ColR).
(* Goal: @Par Tn B1 B2 C1 C2 *)
      apply l12_9 with A1 A2; Perp; CopR.
      }
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
    assert (HParA : Par_strict A1 A2 D1 D2).
(* Goal: @Par Tn A1 A2 D1 D2 *)
      apply par_not_col_strict with D1; Col; apply l12_9 with B1 B2; Perp; CopR.
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
    assert (HParB : Par_strict B1 B2 C1 C2).
(* Goal: @Par Tn B1 B2 C1 C2 *)
      apply par_not_col_strict with C1; Col; apply l12_9 with A1 A2; Perp; CopR.
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
    assert (HNCol3 : ~ Col IAC B1 B2) by (apply par_not_col with C1 C2; Par; ColR).
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
    assert (HNCol4 : ~ Col IBD A1 A2) by (apply par_not_col with D1 D2; Par; ColR).
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
    assert (HPQ : IAC <> IAB) by (assert_diffs; auto).
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
    assert (HQR : IAB <> IBD) by (assert_diffs; auto).
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
    destruct (diff_col_ex3 C1 C2 IAC) as [P1 [HC1P1 [HC2P1 [HPP1 HCP1]]]]; Col.
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
    destruct (diff_col_ex3 D1 D2 IBD) as [R1 [HD1R1 [HD2R1 [HRR1 HDR1]]]]; Col.
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
    destruct (bla IAC IAB IBD P1 R1) as [I [HI1 HI2]]; auto.
      apply perp_per_2; apply perp_col2 with A1 A2; Col;
      apply perp_sym; apply perp_col2 with B1 B2; Col; Perp.
      apply perp_per_2; apply perp_col2 with A1 A2; Col;
      apply perp_sym; apply perp_col2 with C1 C2; Col; Perp.
      apply perp_per_2; apply perp_col2 with B1 B2; Col;
      apply perp_sym; apply perp_col2 with D1 D2; Col; Perp.
(* Goal: @Coplanar Tn IAC IAB IBD P1 *)
(* Goal: @Coplanar Tn IAC IAB IBD R1 *)
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
      assert_diffs; apply col_cop2__cop with C1 C2; Col; CopR.
(* Goal: @Coplanar Tn IAC IAB IBD R1 *)
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
      assert_diffs; apply col_cop2__cop with D1 D2; Col; CopR.
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
    exists I.
(* Goal: and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I) *)
    split; assert_diffs; ColR.
    }

(* Goal: @Saccheri Tn E F S R *)
(* Goal: @Perp Tn C D P Q *)
    {
(* Goal: @bachmann_s_lotschnittaxiom Tn *)
    apply weak_triangle_circumscription_principle__bachmann_s_lotschnittaxiom.
(* Goal: @weak_triangle_circumscription_principle Tn *)
    apply thales_converse_postulate__weak_triangle_circumscription_principle.
(* Goal: @thales_converse_postulate Tn *)
    apply thales_postulate__thales_converse_postulate.
(* Goal: @thales_postulate Tn *)
    apply rah__thales_postulate; assumption.
    }
  }
(* Goal: @Perp Tn C D P Q *)
assert (HNC : ~ Col E R F).
(* Goal: @Saccheri Tn E F S R *)
(* Goal: @Perp Tn C D P Q *)
  {
  assert_diffs; intro; destruct HParS as [_ [_ [_ HF]]];
  apply HF; exists F; split; Col; ColR.
  }
(* Goal: @Perp Tn C D P Q *)
assert (~ Col C D R).
(* Goal: @Saccheri Tn E F S R *)
(* Goal: @Perp Tn C D P Q *)
  {
  assert_diffs; intro; destruct HParS as [_ [_ [_ HF]]];
  apply HF; exists R; split; Col; ColR.
  }
(* Goal: @Perp Tn C D P Q *)
assert (Col E R A) by (assert_diffs; ColR).
(* Goal: @Perp Tn C D P Q *)
assert (Coplanar E R F A) by Cop.
(* Goal: @Perp Tn C D P Q *)
assert (Col E R B) by (assert_diffs; ColR).
(* Goal: @Perp Tn C D P Q *)
assert (Coplanar E R F B) by Cop.
(* Goal: @Perp Tn C D P Q *)
assert (~ Col A B F) by (assert_diffs; intro; apply HNC; ColR).
assert (Coplanar A B F C)
  by (assert_diffs; apply col2_cop__cop with C D;
      try (apply pars__coplanar); Col).
assert (Coplanar A B F D)
  by (assert_diffs; apply col2_cop__cop with C D;
      try (apply pars__coplanar); Col).
assert (Coplanar C D R P)
  by (assert_diffs; apply col2_cop__cop with P Q; Col; Cop).
assert (Coplanar C D R Q)
  by (assert_diffs; apply col2_cop__cop with P Q; Col; Cop).
(* Goal: @Perp Tn C D P Q *)
assert (Coplanar A B Q F) by CopR.
(* Goal: @Perp Tn C D P Q *)
assert (Coplanar E R F P) by CopR.
(* Goal: @Perp Tn C D P Q *)
assert (Coplanar E R F Q) by CopR.
(* Goal: @Perp Tn C D P Q *)
assert (Coplanar E R F C) by CopR.
(* Goal: @Perp Tn C D P Q *)
assert (Coplanar E R F D) by CopR.
(* Goal: @Perp Tn C D P Q *)
assert (Coplanar A B Q E) by Cop.
destruct (HP' A B E F P Q C D E R F) as [S [HC7 HC8]]; Col;
[apply perp_col0 with F M2; try (apply perp_sym; apply per_perp);
 try solve [assert_diffs; assert_cols; Col; ColR];
 rewrite (lam_per__rah M1 _ _ _); try apply lam_perm; assumption|].
(* Goal: @Perp Tn C D P Q *)
assert (HSacc3 : Saccheri E F S R).
(* Goal: @Saccheri Tn E F S R *)
(* Goal: @Perp Tn C D P Q *)
  {
(* Goal: @Saccheri Tn E F S R *)
  split; [apply perp_per_1; apply perp_col0 with A B; Perp|].
  split; [apply perp_per_1; apply perp_col0 with P Q; try apply perp_col0 with A B; Perp;
          intro; treat_equalities; destruct HParS as [_ [_ [_ HF]]];
          exfalso; apply HF; exists S; Col|].
  split; [assert (Cong E F R S); Cong; apply HP with A B C D; Col;
          apply perp_col0 with P Q; Perp; intro; treat_equalities;
          destruct HParS as [_ [_ [_ HF]]]; exfalso; apply HF; exists R; Col|].
  apply l12_6; apply par_strict_col2_par_strict with C D; Col;
  try solve [assert_diffs; assert_cols; Col; ColR];
  try apply par_strict_symmetry;
  try apply par_strict_col2_par_strict with A B; Col; Par.
  intro; treat_equalities; assert (HC8 : Col E P Q)
    by (apply col_cop2_perp2__col with F A B; Col; Perp; Cop).
  apply HD1; elim (perp_not_col2 _ _ _ _ HPerp2); intro;
  [apply l6_21 with A B E F|apply l6_21 with A B F E];
  assert_diffs; Col; try ColR.
  }
(* Goal: @Perp Tn C D P Q *)
apply perp_col0 with S R; try solve [assert_diffs; assert_cols; Col; ColR].
(* Goal: @Perp Tn S R C D *)
apply perp_col0 with F S; try solve [assert_diffs; assert_cols; Col; ColR].
(* Goal: @Perp Tn F S S R *)
apply per_perp; try solve[apply sac_distincts in HSacc3; spliter; auto].
(* Goal: @Per Tn F S R *)
apply l8_2; apply HRAH with E; apply sac_perm; assumption.
Qed.

End universal_posidonius_postulate_perpendicular_transversal_postulate.