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

Section weak_tarski_s_parallel_postulate_weak_inverse_projection_postulate.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

(** Formalization of a proof from Bachmann's article "Zur Parallelenfrage" *)

Lemma  weak_tarski_s_parallel_postulate__weak_inverse_projection_postulate_aux :
  weak_tarski_s_parallel_postulate ->
  forall A B C P T,
    Per A B C -> InAngle T A B C ->
    P <> T -> CongA P B A P B C -> Per B P T -> Coplanar A B C P ->
    (exists X, Out B A X /\ Col T P X) \/ (exists Y, Out B C Y /\ Col T P Y).
Proof.
  intros tora A B C P T HPer HInAngle HPT HCongA HPerP HCop.

  assert (HIn : InAngle P A B C)
    by (apply conga_cop_inangle_per2__inangle with T; assumption).
  assert (HAcute : Acute P B A)
    by (apply acute_sym, conga_inangle_per__acute with C; assumption).
  assert (HAcute' : Acute P B C) by (apply (acute_conga__acute P B A); assumption).
(* Goal: @ex (@Tpoint Tn) (fun Q' : @Tpoint Tn => and (@Col Tn P Q Q') (@Col Tn B C Q')) *)
  assert_diffs.
  assert (HPerp : Perp B P P T) by (apply per_perp; auto).
  assert (HNCol : ~ Col A B C) by (apply per_not_col; auto).
  assert (HNCol1 : ~ Col B P T) by (apply per_not_col; auto).
  destruct (col_dec A B T).
    left; exists T; split; Col.
    apply l6_6, acute_col_perp__out_1 with P; Col.
  destruct (tora A B C T) as [U [V [HU [HV HUTV]]]]; trivial.
  destruct (col_dec P T U) as [HCol|HNCol2].
    left; exists U; split; Col.
  destruct (col_dec P T V) as [HCol|HNCol3].
    right; exists V; split; Col.
  destruct (cop__one_or_two_sides P T B U) as [HTS|HOS]; Col.

(* Goal: @Out Tn B A X *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Col Tn T P X) (and (@Out Tn B C Y) (@Col Tn T P Y))))) *)
    {
    assert (Coplanar A B C P) by Cop.
    assert (Coplanar A B C T) by Cop.
    assert (Coplanar A B U C) by (apply col__coplanar; assert_cols; Col).
(* Goal: @Coplanar Tn C B J P *)
(* Goal: @Per Tn B P Q' *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B C Y) (@Col Tn P Q Y)) *)
    CopR.
    }
    destruct HTS as [_ [_ [X [HX1 HX2]]]].
    left; exists X; split; Col.
    apply l6_7 with U; auto.
    assert_diffs; apply l6_6, bet_out; auto.
    intro; subst; apply HNCol1, HX1.
  assert (HTS : TS P T B V).
    apply l9_8_2 with U; Side.
    repeat split; Col.
    exists T; repeat split; Col.
  destruct HTS as [_ [_ [Y [HY1 HY2]]]].
  right; exists Y; split; Col.
  apply l6_7 with V; auto.
  assert_diffs; apply l6_6, bet_out; auto.
  intro; subst; apply HNCol1, HY1.
Qed.

Lemma weak_tarski_s_parallel_postulate__weak_inverse_projection_postulate :
  weak_tarski_s_parallel_postulate -> weak_inverse_projection_postulate.
Proof.
(* Goal: forall _ : @weak_tarski_s_parallel_postulate Tn, @weak_inverse_projection_postulate Tn *)
intro wtpp.
cut (forall A B C P T,
       Per A B C -> InAngle T A B C ->
       P <> T -> CongA P B A P B C -> Coplanar A B C P -> Per B P T ->
       exists X Y, Out B A X /\ Col T P X /\ Out B C Y /\ Col T P Y).

(* Goal: @Out Tn B A X *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Col Tn T P X) (and (@Out Tn B C Y) (@Col Tn T P Y))))) *)
  {
(* Goal: forall _ : forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : not (@eq (@Tpoint Tn) P T)) (_ : @CongA Tn P B A P B C) (_ : @Coplanar Tn A B C P) (_ : @Per Tn B P T), @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Col Tn T P X) (and (@Out Tn B C Y) (@Col Tn T P Y))))), @weak_inverse_projection_postulate Tn *)
  intros rabp A B C D E F P Q HAcute HPerE HSuma HOut HPQ HPerP HCop.
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B C Y) (@Col Tn P Q Y)) *)
  assert (HNCol1 : ~ Col A B C).
(* Goal: not (@Col Tn A B C) *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B C Y) (@Col Tn P Q Y)) *)
    intro; suma.assert_diffs; apply (per_not_col D E F); auto.
(* Goal: @Col Tn D E F *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B C Y) (@Col Tn P Q Y)) *)
    apply (col2_suma__col A B C A B C); assumption.
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B C Y) (@Col Tn P Q Y)) *)
  assert (HNCol2 : ~ Col B P Q) by (assert_diffs; apply per_not_col; auto).
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B C Y) (@Col Tn P Q Y)) *)
  assert (HCongA : CongA A B C P B C).
(* Goal: @CongA Tn A B C P B C *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B C Y) (@Col Tn P Q Y)) *)
    assert_diffs; apply out_conga with A C A C; try (apply out_trivial); CongA.
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B C Y) (@Col Tn P Q Y)) *)
  assert (HNCol3 : ~ Col P B C) by (apply (ncol_conga_ncol A B C); assumption).
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B C Y) (@Col Tn P Q Y)) *)
  assert (HPerp : Perp B P P Q) by (apply per_perp; assert_diffs; auto).
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B C Y) (@Col Tn P Q Y)) *)
  apply suma_left_comm in HSuma.
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B C Y) (@Col Tn P Q Y)) *)
  destruct HSuma as [J [HJ1 [HJ2 [HJ3 HJ4]]]].
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B C Y) (@Col Tn P Q Y)) *)
  assert (HQ' : exists Q', P <> Q' /\ Col P Q Q' /\ InAngle Q' C B P).
(* Goal: @Out Tn B A X *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Col Tn T P X) (and (@Out Tn B C Y) (@Col Tn T P Y))))) *)
  { destruct (cop_not_par_same_side B P Q P P C) as [Q0 [HCol HOS]]; Col.

(* Goal: @Out Tn B A X *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Col Tn T P X) (and (@Out Tn B C Y) (@Col Tn T P Y))))) *)
      {
(* Goal: @Coplanar Tn C B J P *)
(* Goal: @Per Tn B P Q' *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B C Y) (@Col Tn P Q Y)) *)
      assert (Coplanar A B P C) by Cop.
(* Goal: @Coplanar Tn C B J P *)
(* Goal: @Per Tn B P Q' *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B C Y) (@Col Tn P Q Y)) *)
      CopR.
      }

(* Goal: @ex (@Tpoint Tn) (fun Q' : @Tpoint Tn => and (not (@eq (@Tpoint Tn) P Q')) (and (@Col Tn P Q Q') (@InAngle Tn Q' C B P))) *)
    destruct (one_side_dec B C P Q0).
(* Goal: @ex (@Tpoint Tn) (fun Q' : @Tpoint Tn => and (not (@eq (@Tpoint Tn) P Q')) (and (@Col Tn P Q Q') (@InAngle Tn Q' C B P))) *)
(* Goal: @ex (@Tpoint Tn) (fun Q' : @Tpoint Tn => and (not (@eq (@Tpoint Tn) P Q')) (and (@Col Tn P Q Q') (@InAngle Tn Q' C B P))) *)
      exists Q0; assert_diffs; split; auto; split; Col.
(* Goal: @InAngle Tn Q0 C B P *)
(* Goal: @ex (@Tpoint Tn) (fun Q' : @Tpoint Tn => and (not (@eq (@Tpoint Tn) P Q')) (and (@Col Tn P Q Q') (@InAngle Tn Q' C B P))) *)
      apply os2__inangle; assumption.
(* Goal: @ex (@Tpoint Tn) (fun Q' : @Tpoint Tn => and (not (@eq (@Tpoint Tn) P Q')) (and (@Col Tn P Q Q') (@InAngle Tn Q' C B P))) *)
    assert (HQ' : exists Q', Col P Q Q' /\ Col B C Q').
(* Goal: @Out Tn B A X *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Col Tn T P X) (and (@Out Tn B C Y) (@Col Tn T P Y))))) *)
    { destruct (col_dec B C Q0).
(* Goal: @ex (@Tpoint Tn) (fun Q' : @Tpoint Tn => and (@Col Tn P Q Q') (@Col Tn B C Q')) *)
(* Goal: @ex (@Tpoint Tn) (fun Q' : @Tpoint Tn => and (@Col Tn P Q Q') (@Col Tn B C Q')) *)
        exists Q0; Col.
(* Goal: @ex (@Tpoint Tn) (fun Q' : @Tpoint Tn => and (@Col Tn P Q Q') (@Col Tn B C Q')) *)
      assert_diffs.
(* Goal: @ex (@Tpoint Tn) (fun Q' : @Tpoint Tn => and (@Col Tn P Q Q') (@Col Tn B C Q')) *)
      destruct (cop__not_one_side_two_sides B C P Q0) as [_ [_ [Q' [HCol' HBet]]]]; Col; Cop.
(* Goal: @ex (@Tpoint Tn) (fun Q' : @Tpoint Tn => and (@Col Tn P Q Q') (@Col Tn B C Q')) *)
      exists Q'; split; ColR.
    }
(* Goal: @ex (@Tpoint Tn) (fun Q' : @Tpoint Tn => and (not (@eq (@Tpoint Tn) P Q')) (and (@Col Tn P Q Q') (@InAngle Tn Q' C B P))) *)
    destruct HQ' as [Q' [HCol1 HCol2]].
(* Goal: @ex (@Tpoint Tn) (fun Q' : @Tpoint Tn => and (not (@eq (@Tpoint Tn) P Q')) (and (@Col Tn P Q Q') (@InAngle Tn Q' C B P))) *)
    exists Q'.
(* Goal: and (not (@eq (@Tpoint Tn) P Q')) (and (@Col Tn P Q Q') (@InAngle Tn Q' C B P)) *)
    assert (P <> Q') by (intro; subst; apply HNCol3; Col).
(* Goal: and (not (@eq (@Tpoint Tn) P Q')) (and (@Col Tn P Q Q') (@InAngle Tn Q' C B P)) *)
    split; auto; split; Col.
(* Goal: @InAngle Tn Q' C B P *)
    apply out321__inangle; auto.
(* Goal: not (@TS Tn C B A J) *)
      assert_diffs; auto.
(* Goal: @Out Tn B C Q' *)
    apply l6_6, (acute_col_perp__out_1 P); Col.
(* Goal: @Acute Tn P B C *)
(* Goal: @Perp Tn B P P Q' *)
      apply (acute_conga__acute A B C); assumption.
(* Goal: @Perp Tn B P P Q' *)
    apply perp_col1 with Q; auto.
  }
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B C Y) (@Col Tn P Q Y)) *)
  destruct HQ' as [Q' [HPQ' [HCol HInangle]]].
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B C Y) (@Col Tn P Q Y)) *)
  assert (HInangle' : InAngle Q' C B J).
(* Goal: @Out Tn B A X *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Col Tn T P X) (and (@Out Tn B C Y) (@Col Tn T P Y))))) *)
  { apply in_angle_trans with P; trivial.
(* Goal: @InAngle Tn P C B J *)
    apply l11_25 with A C J; try (apply out_trivial; assert_diffs; auto); [|apply l6_6; assumption].
(* Goal: @InAngle Tn A C B J *)
    apply os_ts__inangle.
(* Goal: @TS Tn B A C J *)
(* Goal: @OS Tn B C J A *)
      assert (~ Col A B J) by (apply (ncol_conga_ncol A B C); CongA).
(* Goal: @TS Tn B A C J *)
(* Goal: @OS Tn B C J A *)
      assert_diffs; apply cop__not_one_side_two_sides; Col; Cop.
(* Goal: @OS Tn B C J A *)
    assert (~ Col C B J).
(* Goal: not (@Col Tn C B J) *)
(* Goal: @OS Tn B C J A *)
      apply (ncol_conga_ncol D E F); CongA; assert_diffs; apply per_not_col; auto.
(* Goal: @OS Tn B C J A *)
    apply invert_one_side, one_side_symmetry, cop__not_two_sides_one_side; Col.
(* Goal: not (@TS Tn C B A J) *)
      assert_diffs; auto.
(* Goal: not (@TS Tn C B A J) *)
    apply conga_sams_nos__nts with A B C; SumA.
  }
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B C Y) (@Col Tn P Q Y)) *)
  destruct (rabp C B J P Q') as [Y [_ [HY1 [HY2 _]]]]; trivial.
(* Goal: @Per Tn C B J *)
(* Goal: @CongA Tn P B C P B J *)
(* Goal: @Coplanar Tn C B J P *)
(* Goal: @Per Tn B P Q' *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B C Y) (@Col Tn P Q Y)) *)
    apply (l11_17 D E F); CongA.
(* Goal: @CongA Tn P B C P B J *)
(* Goal: @Coplanar Tn C B J P *)
(* Goal: @Per Tn B P Q' *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B C Y) (@Col Tn P Q Y)) *)
    assert_diffs; apply out_conga with A C A J; try (apply out_trivial); CongA.
(* Goal: @Coplanar Tn C B J P *)
(* Goal: @Per Tn B P Q' *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B C Y) (@Col Tn P Q Y)) *)
    assert (Coplanar A B P C) by Cop.
(* Goal: @Coplanar Tn C B J P *)
(* Goal: @Per Tn B P Q' *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B C Y) (@Col Tn P Q Y)) *)
    CopR.
(* Goal: @Per Tn B P Q' *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B C Y) (@Col Tn P Q Y)) *)
    apply per_col with Q; auto.
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B C Y) (@Col Tn P Q Y)) *)
  exists Y; split; ColR.
  }

(* Goal: @Out Tn B A X *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Col Tn T P X) (and (@Out Tn B C Y) (@Col Tn T P Y))))) *)
  {
(* Goal: forall (A B C P T : @Tpoint Tn) (_ : @Per Tn A B C) (_ : @InAngle Tn T A B C) (_ : not (@eq (@Tpoint Tn) P T)) (_ : @CongA Tn P B A P B C) (_ : @Coplanar Tn A B C P) (_ : @Per Tn B P T), @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Col Tn T P X) (and (@Out Tn B C Y) (@Col Tn T P Y))))) *)
  intros A B C P T HPer HInAngle HPT HCongA HCop HPerP.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Col Tn T P X) (and (@Out Tn B C Y) (@Col Tn T P Y))))) *)
  assert (HNOut : ~ Out B A C) by (intro; assert_diffs; apply (per_not_col A B C); Col).
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Col Tn T P X) (and (@Out Tn B C Y) (@Col Tn T P Y))))) *)
  assert (HPerp : Perp B P P T) by (assert_diffs; apply per_perp; auto).
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Col Tn T P X) (and (@Out Tn B C Y) (@Col Tn T P Y))))) *)
  destruct (weak_tarski_s_parallel_postulate__weak_inverse_projection_postulate_aux wtpp A B C P T) as [[X [HX1 HX2]]|[Y [HY1 HY2]]]; trivial.
  - destruct (symmetric_point_construction X P) as [Y HY].
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Col Tn T P X) (and (@Out Tn B C Y) (@Col Tn T P Y))))) *)
    assert (X <> Y).
(* Goal: @Out Tn B A X *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Col Tn T P X) (and (@Out Tn B C Y) (@Col Tn T P Y))))) *)
    { intro; treat_equalities.
(* Goal: False *)
      apply HNOut, l6_7 with P; trivial.
(* Goal: @Out Tn B P C *)
      apply (l11_21_a P B A); trivial.
(* Goal: @Out Tn B P A *)
      apply l6_6, HX1.
    }
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Col Tn T P X) (and (@Out Tn B C Y) (@Col Tn T P Y))))) *)
    assert (Out B C Y).
(* Goal: @Out Tn B A X *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Col Tn T P X) (and (@Out Tn B C Y) (@Col Tn T P Y))))) *)
    { apply conga_cop_out_reflectl__out with A P X; trivial.
(* Goal: @ReflectL Tn Y X B P *)
      apply l10_4_spec; split.
(* Goal: @ex (@Tpoint Tn) (fun X0 : @Tpoint Tn => and (@Midpoint Tn X0 Y X) (@Col Tn B P X0)) *)
(* Goal: or (@Perp Tn B P Y X) (@eq (@Tpoint Tn) Y X) *)
        exists P; Col.
(* Goal: or (@Perp Tn B P X Y) (@eq (@Tpoint Tn) X Y) *)
      left; apply perp_col2_bis with P T; ColR.
    }
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Col Tn T P X) (and (@Out Tn B C Y) (@Col Tn T P Y))))) *)
    exists X, Y; repeat (split; try ColR).
  - destruct (symmetric_point_construction Y P) as [X HX].
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Col Tn T P X) (and (@Out Tn B C Y) (@Col Tn T P Y))))) *)
    assert (X <> Y).
(* Goal: @Out Tn B A X *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Col Tn T P X) (and (@Out Tn B C Y) (@Col Tn T P Y))))) *)
    { intro; treat_equalities.
(* Goal: False *)
      apply HNOut, l6_7 with P; apply l6_6; trivial.
(* Goal: @Out Tn B P A *)
      apply (l11_21_a P B C); CongA.
(* Goal: @Out Tn B P C *)
      apply l6_6, HY1.
    }
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Col Tn T P X) (and (@Out Tn B C Y) (@Col Tn T P Y))))) *)
    assert (Out B A X).
(* Goal: @Out Tn B A X *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Col Tn T P X) (and (@Out Tn B C Y) (@Col Tn T P Y))))) *)
    { apply conga_cop_out_reflectl__out with C P Y; CongA; Cop.
(* Goal: not (@Out Tn B C A) *)
(* Goal: @ReflectL Tn Y X B P *)
        intro HOut; apply HNOut, l6_6, HOut.
(* Goal: @ReflectL Tn Y X B P *)
      apply l10_4_spec; split.
(* Goal: @ex (@Tpoint Tn) (fun X0 : @Tpoint Tn => and (@Midpoint Tn X0 Y X) (@Col Tn B P X0)) *)
(* Goal: or (@Perp Tn B P Y X) (@eq (@Tpoint Tn) Y X) *)
        exists P; Col.
(* Goal: or (@Perp Tn B P Y X) (@eq (@Tpoint Tn) Y X) *)
      left; apply perp_col2_bis with P T; try ColR.
    }
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Col Tn T P X) (and (@Out Tn B C Y) (@Col Tn T P Y))))) *)
    exists X, Y; repeat (split; try ColR).
  }
Qed.

End weak_tarski_s_parallel_postulate_weak_inverse_projection_postulate.