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

Section weak_triangle_circumscription_principle_bachmann_s_lotschnittaxiom.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma weak_triangle_circumscription_principle__bachmann_s_lotschnittaxiom :
  weak_triangle_circumscription_principle -> bachmann_s_lotschnittaxiom.
Proof.
(* Goal: forall _ : @weak_triangle_circumscription_principle Tn, @bachmann_s_lotschnittaxiom Tn *)
intro HP.
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 (@eq (@Tpoint Tn) IAB F) *)
(* Goal: @Perp Tn E IAB IAB F *)
  {
(* 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 *)
  intros lotschnitt 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: not (@eq (@Tpoint Tn) IAB F) *)
(* Goal: @Perp Tn E IAB IAB F *)
  {
(* 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 HPerp1 HPerp2 HPerp3.
(* 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 HNC.
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
  destruct (symmetric_point_construction IAB IAC) as [E HE].
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
  destruct (symmetric_point_construction IAB IBD) as [F HF].
(* 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 (HPerp4 : Perp E IAB IAB F).
(* Goal: not (@eq (@Tpoint Tn) IAB F) *)
(* Goal: @Perp Tn E IAB IAB F *)
    {
(* Goal: @Perp Tn E IAB IAB F *)
    assert (E <> IAB).
(* Goal: not (@eq (@Tpoint Tn) IAB F) *)
(* Goal: @Perp Tn E IAB IAB F *)
      {
(* Goal: not (@eq (@Tpoint Tn) IAB F) *)
      intro; treat_equalities; apply HNC; Col.
      }
(* Goal: @Perp Tn E IAB IAB F *)
    assert (IAB <> F).
(* Goal: not (@eq (@Tpoint Tn) IAB F) *)
(* Goal: @Perp Tn E IAB IAB F *)
      {
(* Goal: not (@eq (@Tpoint Tn) IAB F) *)
      intro; treat_equalities; apply HNC; Col.
      }
    apply perp_col0 with B1 B2; try (apply perp_col0 with A1 A2); Col;
    assert_diffs; assert_cols; 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 E) 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 F) by Cop.
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
  assert (Coplanar E F IAB D1) by CopR.
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
  assert (Coplanar E F IAB D2) by CopR.
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
  assert (Coplanar E F IAB C1) by CopR.
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn C1 C2 I) (@Col Tn D1 D2 I)) *)
  assert (Coplanar E F IAB C2) by CopR.
  destruct (HP E F IAB D1 D2 C1 C2) as [I [HC7 HC8]]; auto; try (exists 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; [exists IBD; split; Col| |exists IAC; 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.