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_bachmann_s_lotschnittaxiom.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

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

Lemma weak_inverse_projection_postulate__bachmann_s_lotschnittaxiom :
  weak_inverse_projection_postulate -> bachmann_s_lotschnittaxiom.
Proof.
(* Goal: forall _ : @weak_inverse_projection_postulate Tn, @bachmann_s_lotschnittaxiom Tn *)
intro hrap.
cut (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: @ex (@Tpoint Tn) (fun D3 : @Tpoint Tn => and (@Col Tn D1 D2 D3) (@OS Tn R Q P D3)) *)
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
  {
(* Goal: forall _ : 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)), @bachmann_s_lotschnittaxiom Tn *)
  clear hrap; intro lotschnitt.
(* Goal: @bachmann_s_lotschnittaxiom Tn *)
  intros P Q R P1 R1 HPQ HQR HPerQ HPerP HPerR HCop1 HCop2.
(* Goal: @ex (@Tpoint Tn) (fun S : @Tpoint Tn => and (@Col Tn P P1 S) (@Col Tn R R1 S)) *)
  destruct (eq_dec_points P P1).
(* Goal: @ex (@Tpoint Tn) (fun S : @Tpoint Tn => and (@Col Tn P P1 S) (@Col Tn R R1 S)) *)
(* Goal: @ex (@Tpoint Tn) (fun S : @Tpoint Tn => and (@Col Tn P P1 S) (@Col Tn R R1 S)) *)
    subst; exists R; Col.
(* Goal: @ex (@Tpoint Tn) (fun S : @Tpoint Tn => and (@Col Tn P P1 S) (@Col Tn R R1 S)) *)
  destruct (eq_dec_points R R1).
(* Goal: @ex (@Tpoint Tn) (fun S : @Tpoint Tn => and (@Col Tn P P1 S) (@Col Tn R R1 S)) *)
(* Goal: @ex (@Tpoint Tn) (fun S : @Tpoint Tn => and (@Col Tn P P1 S) (@Col Tn R R1 S)) *)
    subst; exists P; Col.
(* Goal: @ex (@Tpoint Tn) (fun S : @Tpoint Tn => and (@Col Tn P P1 S) (@Col Tn R R1 S)) *)
  assert (HNCol : ~ Col P Q R) by (apply per_not_col; auto).
(* Goal: @ex (@Tpoint Tn) (fun S : @Tpoint Tn => and (@Col Tn P P1 S) (@Col Tn R R1 S)) *)
  destruct (lotschnitt P Q Q R P P1 R R1 Q P R) as [S [HS1 HS2]]; Col; Perp; Cop.
(* Goal: @ex (@Tpoint Tn) (fun S : @Tpoint Tn => and (@Col Tn P P1 S) (@Col Tn R R1 S)) *)
  exists S; auto.
  }

(* Goal: @ex (@Tpoint Tn) (fun D3 : @Tpoint Tn => and (@Col Tn D1 D2 D3) (@OS Tn R Q P D3)) *)
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
  {
(* 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)) *)
  intros 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: @ex (@Tpoint Tn) (fun D3 : @Tpoint Tn => and (@Col Tn D1 D2 D3) (@OS Tn R Q P D3)) *)
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
    {
    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: @ex (@Tpoint Tn) (fun D3 : @Tpoint Tn => and (@Col Tn D1 D2 D3) (@OS Tn R Q P D3)) *)
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
    {
    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 (HNCol5 : ~ Col IAB C1 C2) by (apply par_not_col with B1 B2; Par; ColR).
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
  assert (HNCol6 : ~ Col IAB D1 D2) by (apply par_not_col with A1 A2; 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)) *)
  rename IAB into Q; rename IAC into P; rename IBD into R.
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
  assert (Per P Q R).
(* Goal: @ex (@Tpoint Tn) (fun D3 : @Tpoint Tn => and (@Col Tn D1 D2 D3) (@OS Tn R Q P D3)) *)
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
    {
    apply perp_per_2; apply perp_col2 with A1 A2; Col;
    apply perp_sym; apply perp_col2 with B1 B2; Col; Perp.
    }
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
  assert (HNCol7 : ~ Col P Q R) by (apply per_not_col; trivial).
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
  destruct (angle_bisector P Q R) as [M [HM1 HM2]]; auto.
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
  assert (HSuma : SumA P Q M P Q M P Q R).
(* Goal: @SumA Tn P Q M P Q M P Q R *)
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
    assert_diffs; apply conga3_suma__suma with P Q M M Q R P Q R; CongA; SumA.
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
  assert (HAcute : Acute P Q M).
(* Goal: @ex (@Tpoint Tn) (fun D3 : @Tpoint Tn => and (@Col Tn D1 D2 D3) (@OS Tn R Q P D3)) *)
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
  { apply nbet_sams_suma__acute with P Q R; auto.
(* Goal: not (@Bet Tn P Q R) *)
(* Goal: @SAMS Tn P Q M P Q M *)
      intro HBet; apply HNCol7; Col.
(* Goal: @SAMS Tn P Q M P Q M *)
    destruct (sams_dec P Q M P Q M); trivial.
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
    assert_diffs.
(* Goal: @SAMS Tn P Q M P Q M *)
    exfalso; apply (lea__nlta P Q M P Q R).
(* Goal: @LeA Tn P Q M P Q R *)
(* Goal: @LtA Tn P Q R P Q M *)
      exists M; split; CongA.
(* Goal: @LtA Tn P Q R P Q M *)
    apply obtuse_per__lta; trivial.
(* Goal: @Obtuse Tn P Q M *)
    apply nsams__obtuse; auto.
  }

(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
  assert (HC3 : exists C3, Col C1 C2 C3 /\ OS P Q R C3).
(* Goal: @ex (@Tpoint Tn) (fun D3 : @Tpoint Tn => and (@Col Tn D1 D2 D3) (@OS Tn R Q P D3)) *)
(* 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 P) as [C0]; Col; spliter.
(* Goal: @ex (@Tpoint Tn) (fun C3 : @Tpoint Tn => and (@Col Tn C1 C2 C3) (@OS Tn P Q R C3)) *)
    destruct (cop_not_par_same_side P Q C0 P P R) as [C3 []]; Col.
(* Goal: not (@Col Tn P Q C0) *)
(* Goal: @Coplanar Tn P Q C0 R *)
(* Goal: @ex (@Tpoint Tn) (fun C3 : @Tpoint Tn => and (@Col Tn C1 C2 C3) (@OS Tn P Q R C3)) *)
      intro; apply HNCol5; ColR.
(* Goal: @Coplanar Tn P Q C0 R *)
(* Goal: @ex (@Tpoint Tn) (fun C3 : @Tpoint Tn => and (@Col Tn C1 C2 C3) (@OS Tn P Q R C3)) *)
      assert (Coplanar P Q R C0); [|Cop].
(* Goal: @Coplanar Tn P Q R C3 *)
(* 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; Cop.
(* Goal: @ex (@Tpoint Tn) (fun C3 : @Tpoint Tn => and (@Col Tn C1 C2 C3) (@OS Tn P Q R C3)) *)
    exists C3; split; trivial; ColR.
  }
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
  destruct HC3 as [C3 [HCol7 HOS1]].
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
  destruct (hrap P Q M P Q R P C3) as [S [HS1 HS2]]; trivial.
(* Goal: @Out Tn Q R R *)
(* Goal: not (@eq (@Tpoint Tn) R D3) *)
(* Goal: @Per Tn Q R D3 *)
(* Goal: @Coplanar Tn R Q M D3 *)
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
    apply out_trivial; auto.
(* Goal: not (@eq (@Tpoint Tn) R D3) *)
(* Goal: @Per Tn Q R D3 *)
(* Goal: @Coplanar Tn R Q M D3 *)
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
    assert_diffs; auto.
(* Goal: @Per Tn Q P C3 *)
(* Goal: @Coplanar Tn P Q M C3 *)
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
    assert (HP := HPerpAC); destruct HP as [P' [_ [_ [HP1 [HP2 HP3]]]]].
(* Goal: @Per Tn Q P C3 *)
(* Goal: @Coplanar Tn P Q M C3 *)
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
    assert (P = P'); [|treat_equalities; apply HP3; Col].
    elim (perp_not_col2 _ _ _ _ HPerpAC); intro; assert_diffs;
    [apply l6_21 with A1 A2 C1 C2|apply l6_21 with A1 A2 C2 C1]; Col.
(* Goal: @Coplanar Tn R Q M D3 *)
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
    assert (Coplanar P Q R M) by Cop.
(* Goal: @Coplanar Tn P Q M C3 *)
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
    assert (Coplanar P Q R C3); [|CopR].
(* Goal: @Coplanar Tn P Q R C3 *)
(* 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; Cop.

(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
  assert (HD3 : exists D3, Col D1 D2 D3 /\ OS R Q P D3).
(* Goal: @ex (@Tpoint Tn) (fun D3 : @Tpoint Tn => and (@Col Tn D1 D2 D3) (@OS Tn R Q P D3)) *)
(* 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 R) as [D0]; Col; spliter.
(* Goal: @ex (@Tpoint Tn) (fun D3 : @Tpoint Tn => and (@Col Tn D1 D2 D3) (@OS Tn R Q P D3)) *)
    destruct (cop_not_par_same_side R Q D0 R R P) as [D3 []]; Col.
(* Goal: not (@Col Tn R Q D0) *)
(* Goal: @Coplanar Tn R Q D0 P *)
(* Goal: @ex (@Tpoint Tn) (fun D3 : @Tpoint Tn => and (@Col Tn D1 D2 D3) (@OS Tn R Q P D3)) *)
      intro; apply HNCol6; ColR.
(* Goal: @Coplanar Tn R Q D0 P *)
(* Goal: @ex (@Tpoint Tn) (fun D3 : @Tpoint Tn => and (@Col Tn D1 D2 D3) (@OS Tn R Q P D3)) *)
      assert (Coplanar P Q R D0); [|CopR].
(* Goal: @Coplanar Tn P Q R D3 *)
(* 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; Cop.
(* Goal: @ex (@Tpoint Tn) (fun D3 : @Tpoint Tn => and (@Col Tn D1 D2 D3) (@OS Tn R Q P D3)) *)
    exists D3; split; trivial; ColR.
  }
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
  destruct HD3 as [D3 [HCol8 HOS2]].
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
  destruct (hrap R Q M R Q P R D3) as [T [HT1 HT2]]; Perp.
(* Goal: @Acute Tn R Q M *)
(* Goal: @SumA Tn R Q M R Q M R Q P *)
(* Goal: @Out Tn Q R R *)
(* Goal: not (@eq (@Tpoint Tn) R D3) *)
(* Goal: @Per Tn Q R D3 *)
(* Goal: @Coplanar Tn R Q M D3 *)
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
    apply (acute_conga__acute P Q M); CongA.
(* Goal: @SumA Tn R Q M R Q M R Q P *)
(* Goal: @Out Tn Q R R *)
(* Goal: not (@eq (@Tpoint Tn) R D3) *)
(* Goal: @Per Tn Q R D3 *)
(* Goal: @Coplanar Tn R Q M D3 *)
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
    assert_diffs; apply conga3_suma__suma with P Q M P Q M P Q R; CongA.
(* Goal: @Out Tn Q R R *)
(* Goal: not (@eq (@Tpoint Tn) R D3) *)
(* Goal: @Per Tn Q R D3 *)
(* Goal: @Coplanar Tn R Q M D3 *)
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
    apply out_trivial; auto.
(* Goal: not (@eq (@Tpoint Tn) R D3) *)
(* Goal: @Per Tn Q R D3 *)
(* Goal: @Coplanar Tn R Q M D3 *)
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
    assert_diffs; auto.
(* Goal: @Per Tn Q R D3 *)
(* Goal: @Coplanar Tn R Q M D3 *)
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
    assert (HP := HPerpBD); destruct HP as [R' [_ [_ [HR1 [HR2 HR3]]]]].
(* Goal: @Per Tn Q R D3 *)
(* Goal: @Coplanar Tn R Q M D3 *)
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
    assert (R = R'); [|treat_equalities; apply HR3; Col].
    elim (perp_not_col2 _ _ _ _ HPerpBD); intro; assert_diffs;
    [apply l6_21 with B1 B2 D1 D2|apply l6_21 with B1 B2 D2 D1]; Col.
(* Goal: @Coplanar Tn R Q M D3 *)
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
    assert (Coplanar P Q R M) by Cop.
(* Goal: @Coplanar Tn R Q M D3 *)
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
    assert (Coplanar P Q R D3); [|CopR].
(* Goal: @Coplanar Tn P Q R D3 *)
(* 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; Cop.

(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
  assert (HOut : Out Q S T) by (apply l6_7 with M; trivial; apply l6_6; assumption).
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
  assert (HCol9 : Col C1 C2 S) by (assert_diffs; ColR).
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
  assert (HCol10 : Col D1 D2 T) by (assert_diffs; ColR).
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
  destruct (col_dec C1 C2 T).
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
    exists T; Col.
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
  destruct (col_dec D1 D2 S).
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
    exists S; Col.
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
  destruct HOut as [HSQ [HTQ [HBet|HBet]]].
  - assert (HTS : TS C1 C2 R T).
(* Goal: @TS Tn D1 D2 P S *)
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
      apply l9_8_2 with Q.
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
      repeat split; Col; exists S; Col.
(* Goal: @OS Tn C1 C2 Q R *)
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
      apply l12_6, par_strict_col2_par_strict with B1 B2; Par; Col.
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
    assert_diffs.
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
    destruct HTS as [_ [_ [I [HI1 HI2]]]].
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
    exists I; split; ColR.
  - assert (HTS : TS D1 D2 P S).
(* Goal: @TS Tn D1 D2 P S *)
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
      apply l9_8_2 with Q.
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
      repeat split; Col; exists T; Col.
(* Goal: @OS Tn D1 D2 Q P *)
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
      apply l12_6, par_strict_col2_par_strict with A1 A2; Par; Col.
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
    assert_diffs.
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
    destruct HTS as [_ [_ [I [HI1 HI2]]]].
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
    exists I; split; ColR.
  }
Qed.

End weak_inverse_projection_postulate_bachmann_s_lotschnittaxiom.