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

Section bachmann_s_lotschnittaxiom_weak_triangle_circumscription_principle.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma bachmann_s_lotschnittaxiom__weak_triangle_circumscription_principle :
  bachmann_s_lotschnittaxiom -> weak_triangle_circumscription_principle.
Proof.
(* Goal: forall _ : @bachmann_s_lotschnittaxiom Tn, @weak_triangle_circumscription_principle 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_triangle_circumscription_principle Tn *)
  clear bla; intros HP A B C A1 A2 B1 B2 HNC HPer.
(* Goal: forall (_ : @Perp_bisect Tn A1 A2 B C) (_ : @Perp_bisect Tn B1 B2 A C) (_ : @Coplanar Tn A B C A1) (_ : @Coplanar Tn A B C A2) (_ : @Coplanar Tn A B C B1) (_ : @Coplanar Tn A B C B2), @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn A1 A2 I) (@Col Tn B1 B2 I)) *)
  intros HPerpB1 HPerpB2 HCop1 HCop2 HCop3 HCop4.
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn A1 A2 I) (@Col Tn B1 B2 I)) *)
  destruct (perp_bisect_perp _ _ _ _ HPerpB1) as [A3 [HA [_ [HCol1 [HCol2 _]]]]].
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn A1 A2 I) (@Col Tn B1 B2 I)) *)
  destruct (perp_bisect_perp _ _ _ _ HPerpB2) as [B3 [HB [_ [HCol3 [HCol4 _]]]]].
  assert (Coplanar A B C A3)
    by (apply col_cop2__cop with A1 A2; Col; Cop).
  assert (Coplanar A B C B3)
    by (apply col_cop2__cop with B1 B2; Col; Cop).
  destruct (HP B C A C A1 A2 B1 B2 C A3 B3) as [I [? ?]]; try (exists I; Col);
  try solve[apply perp_right_comm; apply per_perp; assert_diffs; Perp];
  try solve[apply perp_sym; apply perp_bisect_perp; auto]; Col; try CopR.
(* Goal: not (@Col Tn C A3 B3) *)
  assert (C <> A3).
(* 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: not (@eq (@Tpoint Tn) C A3) *)
    assert (HC' := HPerpB1).
(* Goal: not (@eq (@Tpoint Tn) C B3) *)
    destruct HC' as [[[C' [HMid HCol]] _] _].
(* Goal: not (@eq (@Tpoint Tn) C B3) *)
    intro; treat_equalities; assert_diffs.
(* Goal: False *)
    assert (C = C'); [|treat_equalities; auto].
    elim (perp_not_col2 _ _ _ _ (perp_bisect_perp _ _ _ _ HPerpB1)); intro HNC';
    [apply l6_21 with A1 A2 B C|apply l6_21 with A1 A2 C B]; Col.
    }
(* Goal: not (@Col Tn C A3 B3) *)
  assert (C <> B3).
(* 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: not (@eq (@Tpoint Tn) C B3) *)
    assert (HC' := HPerpB2).
(* Goal: not (@eq (@Tpoint Tn) C B3) *)
    destruct HC' as [[[C' [HMid HCol]] _] _].
(* Goal: not (@eq (@Tpoint Tn) C B3) *)
    intro; treat_equalities; assert_diffs.
(* Goal: False *)
    assert (C = C'); [|treat_equalities; auto].
    elim (perp_not_col2 _ _ _ _ (perp_bisect_perp _ _ _ _ HPerpB2)); intro HNC';
    [apply l6_21 with B1 B2 A C|apply l6_21 with B1 B2 C A]; Col.
    }
(* Goal: not (@Col Tn C A3 B3) *)
  intro; apply HNC; ColR.
  }

(* 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: @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: 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: @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: 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: @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 (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 IAC IAB IBD P1 *)
(* Goal: @Coplanar Tn IAC IAB IBD R1 *)
(* 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; CopR.
(* Goal: @Coplanar Tn IAC IAB IBD R1 *)
(* 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; 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_triangle_circumscription_principle.