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

Section weak_inverse_projection_postulate_weak_tarski_s_parallel_postulate.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

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

Lemma weak_inverse_projection_postulate__weak_tarski_s_parallel_postulate_aux :
  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: 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) (_ : @Coplanar Tn A B C P), @InAngle Tn P A B C *)
  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: @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_diffs.
(* Goal: @InAngle Tn P A B C *)
  destruct (angle_bisector A B C) as [P' [HInangle' HConga']]; 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))))) *)
  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: @InAngle Tn P A B C *)
  apply l11_25 with P' A C; try (apply out_trivial); auto.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Out Tn B C Y) (@Bet Tn X T Y)))) *)
  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: @Coplanar Tn B P' A T *)
    assert (Coplanar A B C P') by Cop.
(* Goal: @Col Tn B P P' *)
(* Goal: @Out Tn B P P' *)
    apply conga2_cop2__col with A C; trivial; try CopR; intro; apply HNCol1; Col.
(* Goal: @Out Tn B P P' *)
  apply (acute_col_perp__out T); Col.
(* 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) (_ : @Per Tn B P T) (_ : @Coplanar Tn A B C P), @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 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 (@Col Tn P' B A) *)
(* Goal: @LeA Tn T B P' P' B A *)
      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: False *)
(* Goal: @LeA Tn T B P' P' B A *)
      apply HNCol1; ColR.
(* 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].
    - apply l11_31_1; auto.
(* Goal: @Out Tn B T P' *)
      apply col_one_side_out with A; Col.
(* Goal: @OS Tn B A P' T *)
      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: not (@Col Tn A B T) *)
      intro; assert_diffs; apply HNCol2; ColR.
(* Goal: @Coplanar Tn B P' A T *)
    - assert (Coplanar A B C P') by Cop.
(* Goal: @Coplanar Tn P B C T *)
(* 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 T) by Cop.
(* Goal: @Coplanar Tn P B C T *)
(* 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))))) *)
      CopR.
    - 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: @InAngle Tn T P' B A *)
(* Goal: @InAngle Tn T P' B A *)
        apply out341__inangle; auto.
(* Goal: @Out Tn B C T *)
(* Goal: @InAngle Tn T P' B C *)
        apply col_in_angle_out with A; Col.
(* Goal: not (@Out Tn B A C) *)
(* Goal: @Coplanar Tn A B C T0 *)
(* Goal: @ex (@Tpoint Tn) (fun T' : @Tpoint Tn => and (@InAngle Tn T' A B C) (@Perp Tn B T T T')) *)
        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: @TS Tn B P' C A *)
(* Goal: @OS Tn B C P' T *)
        apply invert_two_sides, in_angle_two_sides; Col.
(* Goal: @OS Tn B C P' T *)
      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: @InAngle Tn T P' B A *)
(* Goal: @InAngle Tn T P' B A *)
        apply out341__inangle; auto.
(* Goal: @Out Tn B A T *)
(* Goal: @InAngle Tn T P' B A *)
        apply col_in_angle_out with C; Col.
(* Goal: not (@Out Tn B A C) *)
(* Goal: @Coplanar Tn A B C T0 *)
(* Goal: @ex (@Tpoint Tn) (fun T' : @Tpoint Tn => and (@InAngle Tn T' A B C) (@Perp Tn B T T T')) *)
        intro; apply HNCol1; Col.
(* Goal: @InAngle Tn T P' B A *)
      apply os2__inangle; trivial.
(* Goal: @OS Tn B A P' T *)
      apply invert_one_side, inangle_one_side with C; Col.
  }
(* Goal: @Perp Tn B P' T P *)
  apply perp_col with P; Col.
(* Goal: @Perp Tn B P T P *)
  apply perp_right_comm, per_perp; auto.
Qed.

Lemma weak_inverse_projection_postulate__weak_tarski_s_parallel_postulate :
  weak_inverse_projection_postulate -> weak_tarski_s_parallel_postulate.
Proof.
(* Goal: forall _ : @weak_inverse_projection_postulate Tn, @weak_tarski_s_parallel_postulate Tn *)
intro wipp.
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 -> Per B P T -> Coplanar A B C P ->
       exists X Y, Out B A X /\ Col T P X /\ Out B C Y /\ Col 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) (_ : @Per Tn B P T) (_ : @Coplanar Tn A B C P), @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) (_ : @Per Tn B P T) (_ : @Coplanar Tn A B C P), @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_tarski_s_parallel_postulate Tn *)
  intros rabp A B C T HPer HInAngle.
(* 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_diffs.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Out Tn B C Y) (@Bet Tn X T Y)))) *)
  destruct (angle_bisector A B C) as [P0 [HIn HConga]]; 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))))) *)
  assert_diffs.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Out Tn B C Y) (@Bet Tn X T Y)))) *)
  assert (HNCol1 : ~ Col A B C) by (apply per_not_col; auto).
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Out Tn B C Y) (@Bet Tn X T Y)))) *)
  assert (HNCol2 : ~ Col P0 B A).
(* 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) (_ : @Per Tn B P T) (_ : @Coplanar Tn A B C P), @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 (SumA P0 B A P0 B A A B C) by (apply (conga3_suma__suma A B P0 P0 B C A B C); CongA; SumA).
(* Goal: not (@Col Tn P0 B A) *)
    intro; apply HNCol1, (col2_suma__col P0 B A P0 B A); assumption.
  }
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Out Tn B C Y) (@Bet Tn X T Y)))) *)
  assert (HXY : exists X Y, Out B A X /\ Out B C Y /\ Col X T 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) (_ : @Per Tn B P T) (_ : @Coplanar Tn A B C P), @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 P0 T).
    - assert (HT' : exists T', InAngle T' A B C /\ Perp B T T T').
(* 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) (_ : @Per Tn B P T) (_ : @Coplanar Tn A B C P), @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 (l10_15 B P0 T A) as [T0 [HPerp HOS]]; Col.
(* Goal: @ex (@Tpoint Tn) (fun T' : @Tpoint Tn => and (@InAngle Tn T' A B C) (@Perp Tn B T T T')) *)
        destruct (cop_inangle__ex_col_inangle A B C T T0) as [T' [HT1 [HT2 HT3]]]; trivial.
(* Goal: not (@Out Tn B A C) *)
(* Goal: @Coplanar Tn A B C T0 *)
(* Goal: @ex (@Tpoint Tn) (fun T' : @Tpoint Tn => and (@InAngle Tn T' A B C) (@Perp Tn B T T T')) *)
            intro; apply HNCol1; Col.
(* Goal: @Coplanar Tn A B C P *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Out Tn B C Y) (@Col Tn X T Y)))) *)
          assert (Coplanar P0 A B C) by Cop.
(* Goal: @Coplanar Tn A B C T0 *)
(* Goal: @ex (@Tpoint Tn) (fun T' : @Tpoint Tn => and (@InAngle Tn T' A B C) (@Perp Tn B T T T')) *)
          assert (Coplanar P0 A B T0) by Cop.
(* Goal: @Coplanar Tn P B C T *)
(* 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))))) *)
          CopR.
(* Goal: @ex (@Tpoint Tn) (fun T' : @Tpoint Tn => and (@InAngle Tn T' A B C) (@Perp Tn B T T T')) *)
        exists T'; split; trivial.
(* 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_diffs.
(* Goal: @Perp Tn B T T T' *)
        apply perp_col with P0; Col.
(* Goal: @Perp Tn B P0 T T' *)
        apply perp_col1 with T0; Perp.
      }
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Out Tn B C Y) (@Col Tn X T Y)))) *)
      destruct HT' as [T' []].
(* 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_diffs.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Out Tn B C Y) (@Col Tn X T Y)))) *)
      destruct (rabp A B C T T') as [X [Y]]; Perp; Cop.
(* Goal: @CongA Tn P B A P B C *)
(* Goal: @Per Tn B P T *)
(* Goal: @Coplanar Tn A B C P *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Out Tn B C Y) (@Col Tn X T Y)))) *)
        apply col_conga__conga with P0; auto.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Out Tn B C Y) (@Col Tn X T Y)))) *)
      spliter; exists X, Y; repeat (split; trivial); ColR.
    - destruct (l8_18_existence B P0 T) as [P [HP1 HP2]]; trivial.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Out Tn B C Y) (@Col Tn X T Y)))) *)
      assert (Out B P P0).
(* Goal: @Out Tn B P P0 *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Out Tn B C Y) (@Col Tn X T Y)))) *)
        apply (acute_col_perp__out T); trivial.
(* Goal: @Acute Tn T B P0 *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Out Tn B C Y) (@Col Tn X T Y)))) *)
        apply acute_sym, conga_inangle2_per__acute with A C; trivial.
(* 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_diffs.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Out Tn B C Y) (@Col Tn X T Y)))) *)
      destruct (rabp A B C P T) as [X [Y]]; auto.
(* Goal: @CongA Tn P B A P B C *)
(* Goal: @Per Tn B P T *)
(* Goal: @Coplanar Tn A B C P *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Out Tn B C Y) (@Col Tn X T Y)))) *)
        apply col_conga__conga with P0; auto.
(* Goal: @Per Tn B P T *)
(* Goal: @Coplanar Tn A B C P *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Out Tn B C Y) (@Col Tn X T Y)))) *)
        apply perp_per_1, perp_left_comm, perp_col with P0; auto.
(* Goal: @Coplanar Tn A B C P *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Out Tn B C Y) (@Col Tn X T Y)))) *)
        assert (Coplanar P0 A B C) by Cop.
(* Goal: @Coplanar Tn A B C P *)
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Out Tn B C Y) (@Col Tn X T Y)))) *)
        assert (Coplanar B P0 P A) by Cop.
(* Goal: @Coplanar Tn P B C T *)
(* 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))))) *)
        CopR.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Out Tn B C Y) (@Col Tn X T Y)))) *)
      spliter; exists X, Y; repeat (split; trivial); ColR.
  }
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Out Tn B C Y) (@Bet Tn X T Y)))) *)
  destruct HXY as [X [Y [HOutX [HOutY HCol]]]].
(* 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_diffs.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Out Tn B C Y) (@Bet Tn X T Y)))) *)
  assert (X <> Y) by (intro; subst; apply HNCol1; ColR).
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B A X) (and (@Out Tn B C Y) (@Bet Tn X T Y)))) *)
  exists X, Y; repeat (split; trivial).
(* Goal: @Bet Tn X T Y *)
  destruct (eq_dec_points T X) as [HTX|HTX]; try (subst; Between).
(* Goal: @Bet Tn X T Y *)
  destruct (eq_dec_points T Y) as [HTY|HTY]; try (subst; Between).
(* Goal: @Bet Tn X T Y *)
  apply out2__bet.
  - apply col_one_side_out with B; trivial.
(* Goal: @OS Tn X B T Y *)
    apply invert_one_side, col_one_side with A; Col.
(* Goal: @OS Tn B A T Y *)
    apply out_out_one_side with C; trivial.
(* Goal: @OS Tn B A T C *)
    apply invert_one_side, in_angle_one_side; Col.
(* Goal: not (@Col Tn B A T) *)
    intro; apply HTX, (l6_21 A B Y X); Col.
(* Goal: False *)
(* Goal: @LeA Tn T B P' P' B A *)
    intro; subst; apply HNCol1; ColR.
  - apply col_one_side_out with B; Col.
(* Goal: @OS Tn Y B X T *)
    apply invert_one_side, col_one_side with C; Col.
(* Goal: @OS Tn B C X T *)
    apply one_side_symmetry, out_out_one_side with A; trivial.
(* Goal: @OS Tn B C T A *)
    apply invert_one_side, in_angle_one_side; (try apply l11_24); Col.
(* Goal: not (@Col Tn B C T) *)
    intro; apply HTY, (l6_21 B C X Y); Col.
(* Goal: False *)
(* Goal: @LeA Tn T B P' P' B A *)
    intro; subst; apply HNCol1; ColR.
  }

(* 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) (_ : @Per Tn B P T) (_ : @Coplanar Tn A B C P), @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) (_ : @Per Tn B P T) (_ : @Coplanar Tn A B C P), @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 HPerP HCop.
(* 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_diffs.
(* 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 (HIn : InAngle P A B C) by (apply conga_cop_inangle_per2__inangle with T; assumption).
(* 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 (HSumA : SumA P B A P B A A B C).
(* Goal: @SumA Tn P B A P B A A B C *)
(* 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 (conga3_suma__suma A B P P B C A B C); CongA; SumA.
(* 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 (HAcute : Acute P B A) by (apply acute_sym, conga_inangle_per__acute with C; assumption).
(* 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 (HOut : Out B P P) by (apply out_trivial; 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 (wipp P B A A B C P T) as [X [HX1 HX2]]; trivial.
(* Goal: @Coplanar Tn P B C T *)
(* 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 T) by Cop.
(* Goal: @Coplanar Tn P B C T *)
(* 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 (~ Col A B C) by (apply per_not_col; auto).
(* Goal: @Coplanar Tn P B C T *)
(* 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))))) *)
  CopR.
(* 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 (wipp P B C C B A P T) as [Y [HY1 HY2]]; Perp.
(* Goal: @Acute Tn P B C *)
(* Goal: @SumA Tn P B C P B C C B A *)
(* Goal: @Coplanar Tn P B C T *)
(* 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 (acute_conga__acute P B A); assumption.
(* Goal: @SumA Tn P B C P B C C B A *)
(* Goal: @Coplanar Tn P B C T *)
(* 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 (conga3_suma__suma P B A P B A A B C); CongA.
(* Goal: @Coplanar Tn P B C T *)
(* 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 T) by Cop.
(* Goal: @Coplanar Tn P B C T *)
(* 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 (~ Col A B C) by (apply per_not_col; auto).
(* Goal: @Coplanar Tn P B C T *)
(* 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))))) *)
    CopR.
(* 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; Col).
  }
Qed.

End weak_inverse_projection_postulate_weak_tarski_s_parallel_postulate.