Library GeoCoq.Meta_theory.Parallel_postulates.weak_triangle_circumscription_principle_bachmann_s_lotschnittaxiom

Require Import GeoCoq.Axioms.parallel_postulates.
Require Import GeoCoq.Tarski_dev.Ch13_1.

Section weak_triangle_circumscription_principle_bachmann_s_lotschnittaxiom.

Context `{TD:Tarski_2D}.

Lemma weak_triangle_circumscription_principle__bachmann_s_lotschnittaxiom :
  weak_triangle_circumscription_principle → bachmann_s_lotschnittaxiom.
Proof.
intro HP.
cut (∀ A1 A2 B1 B2 C1 C2 D1 D2,
        Perp A1 A2 B1 B2 → Perp A1 A2 C1 C2 → Perp B1 B2 D1 D2 →
        ¬ Col A1 A2 D1 → ¬ Col B1 B2 C1 →
        ∃ I, Col C1 C2 I ∧ Col D1 D2 I).

  {
  intros lotschnitt P Q R P1 R1 HPQ HQR HPerQ HPerP HPerR.
  destruct (eq_dec_points P P1).
    subst; ∃ R; Col.
  destruct (eq_dec_points R R1).
    subst; ∃ P; Col.
  assert (HNCol : ¬ Col P Q R) by (apply per_not_col; auto).
  destruct (lotschnitt P Q Q R P P1 R R1) as [S [HS1 HS2]]; Col; Perp.
  ∃ S; auto.
  }

  {
  intros A1 A2 B1 B2 C1 C2 D1 D2 HPerp1 HPerp2 HPerp3 HNC1 HNC2.
  destruct (perp_inter_perp_in_n A1 A2 B1 B2) as [AB [HC1 [HC2 _]]]; Perp.
  destruct (perp_inter_perp_in_n A1 A2 C1 C2) as [AC [HC3 [HC4 _]]]; Perp.
  destruct (perp_inter_perp_in_n B1 B2 D1 D2) as [BD [HC5 [HC6 _]]]; Perp.
  destruct (symmetric_point_construction AB AC) as [E HE].
  destruct (symmetric_point_construction AB BD) as [F HF].
  assert (HPerp4 : Perp E AB AB F).
    {
    assert (E ≠ AB).
      {
      intro; treat_equalities; apply HNC2;
      apply not_strict_par1 with C2 AC; Col.
      apply l12_9 with A1 A2; Perp.
      }
    assert (AB ≠ F).
      {
      intro; treat_equalities; apply HNC1;
      apply not_strict_par1 with D2 BD; Col.
      apply l12_9 with B1 B2; Perp.
      }
    apply perp_col0 with B1 B2; try (apply perp_col0 with A1 A2); Col;
    assert_diffs; assert_cols; ColR.
    }
  destruct (HP E F AB D1 D2 C1 C2) as [I [HC7 HC8]]; try (∃ I; Col);
  try (apply not_col_permutation_1; apply perp_not_col); try apply perp_per_1;
  try solve[assert_diffs; Perp]; split; [|assert_diffs| |assert_diffs]; auto;
  split; [∃ BD; split; Col| |∃ AC; split; Col|]; left;
  [apply perp_col0 with B1 B2|apply perp_col0 with A1 A2];
  assert_diffs; Col; ColR.
  }
Qed.

End weak_triangle_circumscription_principle_bachmann_s_lotschnittaxiom.