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

Section bachmann_s_lotschnittaxiom_weak_inverse_projection_postulate.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

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

Lemma bachmann_s_lotschnittaxiom__weak_inverse_projection_postulate :
  bachmann_s_lotschnittaxiom -> weak_inverse_projection_postulate.
Proof.
(* Goal: forall _ : @bachmann_s_lotschnittaxiom Tn, @weak_inverse_projection_postulate Tn *)
intro bla.
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: not (@Col Tn B1 B2 C1) *)
(* 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)), @weak_inverse_projection_postulate Tn *)
  clear bla; intro lotschnitt.
(* Goal: @weak_inverse_projection_postulate Tn *)
  intros A B C D E F P Q HAcute HPer HSuma HOut HPQ HPerP HCop.
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B C Y) (@Col Tn P Q Y)) *)
  suma.assert_diffs.
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B C Y) (@Col Tn P Q Y)) *)
  assert (HNCol : ~ Col A B C).
(* Goal: not (@Col Tn B1 B2 C1) *)
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
  { intro HCol.
(* Goal: False *)
    apply (per_not_col D E F); auto.
(* Goal: @Col Tn D E F *)
    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 (HNCol1 : ~ Col B C P) by (intro; apply HNCol; ColR).
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B C Y) (@Col Tn P Q Y)) *)
  destruct (l10_6_existence_spec B C P) as [P' HP']; trivial.
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B C Y) (@Col Tn P Q Y)) *)
  assert (HP'1 : Reflect P P' B C) by (apply is_image_is_image_spec; auto).
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B C Y) (@Col Tn P Q Y)) *)
  assert (HNCol2 : ~ Col B C P') by (apply osym_not_col with P; trivial).
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B C Y) (@Col Tn P Q Y)) *)
  destruct (l10_6_existence_spec B C Q) as [Q' HQ']; trivial.
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B C Y) (@Col Tn P Q Y)) *)
  assert (HQ'1 : Reflect Q Q' B C) by (apply is_image_is_image_spec; auto).
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B C Y) (@Col Tn P Q Y)) *)
  assert_diffs.
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B C Y) (@Col Tn P Q Y)) *)
  assert (P' <> Q').
(* Goal: not (@eq (@Tpoint Tn) P' Q') *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B C Y) (@Col Tn P Q Y)) *)
   intro; subst Q'; assert (P = Q) by (apply (l10_2_uniqueness B C P'); assumption); auto.
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B C Y) (@Col Tn P Q Y)) *)
  apply l6_6 in HOut.
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B C Y) (@Col Tn P Q Y)) *)
  assert (HCongA : CongA C B P' A B C).
(* Goal: @CongA Tn C B P' A B C *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B C Y) (@Col Tn P Q Y)) *)
    apply out_conga with C P' P C; try (apply out_trivial); auto.
(* Goal: @CongA Tn C B P' P B C *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B C Y) (@Col Tn P Q Y)) *)
    apply conga_sym, conga_left_comm, reflectl__conga; auto.
(* Goal: @ReflectL Tn P P' C B *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B C Y) (@Col Tn P Q Y)) *)
    apply is_image_spec_rev, HP'.
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B C Y) (@Col Tn P Q Y)) *)
  assert (HTS : TS B C P P').
(* Goal: @TS Tn B C P P' *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B C Y) (@Col Tn P Q Y)) *)
    repeat split; Col; destruct HP' as [[X [HX1 HX2]] _]; exists X; split; Col; Between.
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B C Y) (@Col Tn P Q Y)) *)
  assert (HPer1 : Per A B P').
(* Goal: not (@Col Tn B1 B2 C1) *)
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
  { apply l11_17 with D E F; trivial.
(* Goal: @CongA Tn D E F A B P' *)
    apply (suma2__conga A B C A B C); trivial.
(* Goal: @SumA Tn A B C A B C A B P' *)
    apply conga3_suma__suma with A B C C B P' A B P'; CongA.
(* Goal: @SumA Tn A B C C B P' A B P' *)
    exists P'; assert_diffs; repeat (split; CongA).
(* Goal: not (@OS Tn B C A P') *)
(* Goal: @OS Tn A B P' Y *)
      apply l9_9, l9_5 with P B; Col.
(* Goal: @Coplanar Tn A B C P' *)
(* Goal: not (@TS Tn A B C P') *)
(* Goal: @OS Tn A B P' Y *)
      assert (Coplanar P' C A B) by (apply col2_cop__cop with P B; Col; Cop).
(* Goal: @Coplanar Tn A B C P' *)
(* Goal: not (@TS Tn A B C P') *)
(* Goal: @OS Tn A B P' Y *)
      Cop.
  }
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B C Y) (@Col Tn P Q Y)) *)
  assert (HNCol3 : ~ Col A B P') by (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 (HNCol4 : ~ Col B P' P) by (intro; apply HNCol3; ColR).
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B C Y) (@Col Tn P Q Y)) *)
  assert (HPerp1 : Perp A B B P') by (apply per_perp; auto).
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B C Y) (@Col Tn P Q Y)) *)
  assert (HPerp2 : Perp A B P Q) by (apply perp_left_comm, perp_col with P; Col; apply per_perp; auto).
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B C Y) (@Col Tn P Q Y)) *)
  assert (HPerp3 : Perp B P' P' Q').
(* Goal: @Perp Tn B P' P' Q' *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B C Y) (@Col Tn P Q Y)) *)
    apply per_perp; auto; apply image_spec_preserves_per with B P Q B C; trivial; apply col__refl; Col.
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B C Y) (@Col Tn P Q Y)) *)
  assert (HNCol5 : ~ Col P' P Q).
(* Goal: not (@Col Tn P' P Q) *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B C Y) (@Col Tn P Q Y)) *)
    apply (par_not_col B P'); Col.
(* Goal: @Par_strict Tn B P' P Q *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B C Y) (@Col Tn P Q Y)) *)
    apply par_not_col_strict with P; Col.
(* Goal: @Coplanar Tn A B C P' *)
(* Goal: not (@TS Tn A B C P') *)
(* Goal: @OS Tn A B P' Y *)
    apply l12_9 with A B; Perp; Cop.
(* Goal: @Coplanar Tn A B C P' *)
(* Goal: not (@TS Tn A B C P') *)
(* Goal: @OS Tn A B P' Y *)
    assert (Coplanar P' C A B) by (apply col2_cop__cop with P B; Col; Cop).
(* Goal: @Coplanar Tn A 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 Y : @Tpoint Tn => and (@Out Tn B C Y) (@Col Tn P Q Y)) *)
  assert (HI := HPerp2); destruct HI as [I [_ [_ [HCol1 [HCol2 _]]]]].
(* Goal: @Coplanar Tn A B C P' *)
(* Goal: not (@TS Tn A B C P') *)
(* Goal: @OS Tn A B P' Y *)
  assert (Coplanar P' C A B) by (apply col2_cop__cop with P B; Col; Cop).
(* Goal: @Coplanar Tn A B C P' *)
(* Goal: not (@TS Tn A B C P') *)
(* Goal: @OS Tn A B P' Y *)
  assert (Coplanar P C A B) by Cop.
(* Goal: @Coplanar Tn A B C P' *)
(* Goal: not (@TS Tn A B C P') *)
(* Goal: @OS Tn A B P' Y *)
  assert (Coplanar Q Q' B C) by Cop.
(* Goal: @Coplanar Tn A B P' Q *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B C Y) (@Col Tn P Q Y)) *)
  destruct (lotschnitt A B B P' P Q P' Q' B P P') as [Y [HY1 HY2]]; Col; try CopR.

(* Goal: not (@Col Tn B1 B2 C1) *)
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
    {
(* Goal: @Coplanar Tn B P' A Q' *)
    elim (col_dec B C Q); intro; [|CopR].
(* Goal: @Coplanar Tn B P' A Q' *)
    assert (Q = Q'); [|treat_equalities; CopR].
(* Goal: @eq (@Tpoint Tn) Q Q' *)
    apply col_image_spec__eq with B C; Col.
    }

(* Goal: not (@Col Tn B1 B2 C1) *)
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
    {
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B C Y) (@Col Tn P Q Y)) *)
    exists Y; split; trivial.
(* Goal: @Out Tn B C Y *)
    apply col_one_side_out with A.
(* Goal: @Col Tn B C Y *)
(* Goal: @OS Tn B A C Y *)
      apply col_permutation_1, intersection_with_image_gen with P Q P' Q'; Col.
(* Goal: @OS Tn B A C Y *)
    apply invert_one_side, one_side_transitivity with P'.
(* Goal: @OS Tn A B C P' *)
(* Goal: @OS Tn A B P' Y *)
      apply cop__not_two_sides_one_side; Col.
(* Goal: @Coplanar Tn A B C P' *)
(* Goal: not (@TS Tn A B C P') *)
(* Goal: @OS Tn A B P' Y *)
      assert (Coplanar P' C A B) by (apply col2_cop__cop with P B; Col; Cop).
(* Goal: @Coplanar Tn A B C P' *)
(* Goal: not (@TS Tn A B C P') *)
(* Goal: @OS Tn A B P' Y *)
      Cop.
(* Goal: not (@TS Tn A B C P') *)
(* Goal: @OS Tn A B P' Y *)
      apply (conga_sams_nos__nts A B C A B C P'); SumA.
(* Goal: not (@OS Tn B C A P') *)
(* Goal: @OS Tn A B P' Y *)
      apply l9_9, l9_5 with P B; Col.
(* Goal: @OS Tn A B P' Y *)
    apply l12_6, par_strict_col_par_strict with Q'; Col.
(* Goal: not (@eq (@Tpoint Tn) P' Y) *)
(* Goal: @Par_strict Tn A B P' Q' *)
      intro; subst; apply HNCol5; Col.
(* Goal: @Par_strict Tn A B P' Q' *)
    apply par_not_col_strict with P'; Col.
(* Goal: @Coplanar Tn A B C P' *)
(* Goal: not (@TS Tn A B C P') *)
(* Goal: @OS Tn A B P' Y *)
    apply l12_9 with B P'; Perp; Cop.
(* Goal: @Coplanar Tn B P' A Q' *)
    elim (col_dec B C Q); intro; [|CopR].
(* Goal: @Coplanar Tn B P' A Q' *)
    assert (Q = Q'); [|treat_equalities; CopR].
(* Goal: @eq (@Tpoint Tn) Q Q' *)
    apply col_image_spec__eq with B C; Col.
    }
  }

(* Goal: not (@Col Tn B1 B2 C1) *)
(* 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 HNCop1 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: @Coplanar Tn A B C P' *)
(* Goal: not (@TS Tn A B C P') *)
(* Goal: @OS Tn A B P' Y *)
  assert (Coplanar IAB IAC IBD A1) by Cop.
(* Goal: @Coplanar Tn A B C P' *)
(* Goal: not (@TS Tn A B C P') *)
(* Goal: @OS Tn A B P' Y *)
  assert (Coplanar IAB IAC IBD A2) by Cop.
(* Goal: @Coplanar Tn A B C P' *)
(* Goal: not (@TS Tn A B C P') *)
(* Goal: @OS Tn A B P' Y *)
  assert (Coplanar IAB IAC IBD B1) by Cop.
(* Goal: @Coplanar Tn A B C P' *)
(* Goal: not (@TS Tn A B C P') *)
(* Goal: @OS Tn A B P' Y *)
  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: not (@Col Tn B1 B2 C1) *)
(* 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: @Coplanar Tn A B P' Q *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B C Y) (@Col Tn P Q Y)) *)
    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: not (@Col Tn B1 B2 C1) *)
(* 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: @Coplanar Tn A B P' Q *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B C Y) (@Col Tn P Q Y)) *)
    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: @Coplanar Tn A B P' Q *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B C Y) (@Col Tn P Q Y)) *)
    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: @Coplanar Tn A B P' Q *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Out Tn B C Y) (@Col Tn P Q Y)) *)
    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 A 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 col_cop2__cop with C1 C2; Col; CopR.
(* Goal: @Coplanar Tn A 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 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.
  }
Qed.

End bachmann_s_lotschnittaxiom_weak_inverse_projection_postulate.