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

Section par_perp_perp_TCP.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Lemma inter_dec_plus_par_perp_perp_imply_triangle_circumscription :
  decidability_of_intersection ->
  perpendicular_transversal_postulate ->
  triangle_circumscription_principle.
Proof.
(* Goal: forall (_ : @decidability_of_intersection Tn) (_ : @perpendicular_transversal_postulate Tn), @triangle_circumscription_principle Tn *)
intros HID HPTP A B C HNC.
assert (HAB := perp_bisect_existence_cop A B C);
destruct HAB as [C1 [C2 [HAB HCop1]]]; try (assert_diffs; assumption).
assert (HAC := perp_bisect_existence_cop A C B);
destruct HAC as [B1 [B2 [HAC HCop2]]]; try (assert_diffs; assumption).
(* Goal: @ex (@Tpoint Tn) (fun CC : @Tpoint Tn => and (@Cong Tn A CC B CC) (and (@Cong Tn A CC C CC) (@Coplanar Tn A B C CC))) *)
assert (HInter := HID B1 B2 C1 C2).
(* Goal: @ex (@Tpoint Tn) (fun CC : @Tpoint Tn => and (@Cong Tn A CC B CC) (and (@Cong Tn A CC C CC) (@Coplanar Tn A B C CC))) *)
elim HInter; clear HInter; intro HInter.

(* Goal: @ex (@Tpoint Tn) (fun CC : @Tpoint Tn => and (@Cong Tn A CC B CC) (and (@Cong Tn A CC C CC) (@Coplanar Tn A B C CC))) *)
(* Goal: @ex (@Tpoint Tn) (fun CC : @Tpoint Tn => and (@Cong Tn A CC B CC) (and (@Cong Tn A CC C CC) (@Coplanar Tn A B C CC))) *)
  destruct HInter as [CC [HCol1 HCol2]].

(* Goal: @ex (@Tpoint Tn) (fun CC : @Tpoint Tn => and (@Cong Tn A CC B CC) (and (@Cong Tn A CC C CC) (@Coplanar Tn A B C CC))) *)
(* Goal: @ex (@Tpoint Tn) (fun CC : @Tpoint Tn => and (@Cong Tn A CC B CC) (and (@Cong Tn A CC C CC) (@Coplanar Tn A B C CC))) *)
    exists CC; split.

(* Goal: @Cong Tn A CC B CC *)
(* Goal: and (@Cong Tn A CC C CC) (@Coplanar Tn A B C CC) *)
(* Goal: @ex (@Tpoint Tn) (fun CC : @Tpoint Tn => and (@Cong Tn A CC B CC) (and (@Cong Tn A CC C CC) (@Coplanar Tn A B C CC))) *)
      elim (eq_dec_points CC C1); intro HEq; try subst.

(* Goal: @Cong Tn A C1 B C1 *)
(* Goal: @Cong Tn A CC B CC *)
(* Goal: and (@Cong Tn A CC C CC) (@Coplanar Tn A B C CC) *)
(* Goal: @ex (@Tpoint Tn) (fun CC : @Tpoint Tn => and (@Cong Tn A CC B CC) (and (@Cong Tn A CC C CC) (@Coplanar Tn A B C CC))) *)
        apply perp_bisect_cong_1 with C2; assumption.

(* Goal: @Cong Tn A CC B CC *)
(* Goal: and (@Cong Tn A CC C CC) (@Coplanar Tn A B C CC) *)
(* Goal: @ex (@Tpoint Tn) (fun CC : @Tpoint Tn => and (@Cong Tn A CC B CC) (and (@Cong Tn A CC C CC) (@Coplanar Tn A B C CC))) *)
        apply perp_bisect_cong_1 with C1.
(* Goal: @Perp_bisect Tn CC B1 A C *)
(* Goal: @Coplanar Tn A B C CC *)
(* Goal: @ex (@Tpoint Tn) (fun CC : @Tpoint Tn => and (@Cong Tn A CC B CC) (and (@Cong Tn A CC C CC) (@Coplanar Tn A B C CC))) *)
        apply perp_bisect_sym_1.
(* Goal: not (@eq (@Tpoint Tn) C1 C2) *)
(* Goal: @Coplanar Tn B1 B2 C1 C2 *)
(* Goal: not (@ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X B1 B2) (@Col Tn X C1 C2))) *)
(* Goal: @Col Tn A B C *)
        apply perp_bisect_equiv_def in HAB.
(* Goal: not (@eq (@Tpoint Tn) C1 C2) *)
(* Goal: @Coplanar Tn B1 B2 C1 C2 *)
(* Goal: not (@ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X B1 B2) (@Col Tn X C1 C2))) *)
(* Goal: @Col Tn A B C *)
        destruct HAB as [I [HPerp HMid]].
(* Goal: @Perp_bisect Tn B1 CC A C *)
(* Goal: @Coplanar Tn A B C CC *)
(* Goal: @ex (@Tpoint Tn) (fun CC : @Tpoint Tn => and (@Cong Tn A CC B CC) (and (@Cong Tn A CC C CC) (@Coplanar Tn A B C CC))) *)
        apply perp_bisect_equiv_def.
(* Goal: @Perp_bisect_bis Tn B1 CC A C *)
(* Goal: @Coplanar Tn A B C CC *)
(* Goal: @ex (@Tpoint Tn) (fun CC : @Tpoint Tn => and (@Cong Tn A CC B CC) (and (@Cong Tn A CC C CC) (@Coplanar Tn A B C CC))) *)
        exists I; split; try assumption.
(* Goal: @Perp_at Tn I A C B1 B2 *)
(* Goal: @Coplanar Tn A B C CC *)
(* Goal: @ex (@Tpoint Tn) (fun CC : @Tpoint Tn => and (@Cong Tn A CC B CC) (and (@Cong Tn A CC C CC) (@Coplanar Tn A B C CC))) *)
        apply perp_in_sym.
(* Goal: @Perp_at Tn I A B C1 CC *)
(* Goal: and (@Cong Tn A CC C CC) (@Coplanar Tn A B C CC) *)
(* Goal: @ex (@Tpoint Tn) (fun CC : @Tpoint Tn => and (@Cong Tn A CC B CC) (and (@Cong Tn A CC C CC) (@Coplanar Tn A B C CC))) *)
        apply perp_in_col_perp_in with C2; Col.
(* Goal: @Perp_at Tn I A C B1 B2 *)
(* Goal: @Coplanar Tn A B C CC *)
(* Goal: @ex (@Tpoint Tn) (fun CC : @Tpoint Tn => and (@Cong Tn A CC B CC) (and (@Cong Tn A CC C CC) (@Coplanar Tn A B C CC))) *)
        apply perp_in_sym.
(* Goal: @Perp_at Tn I B1 B2 A C *)
(* Goal: @Coplanar Tn A B C CC *)
(* Goal: @ex (@Tpoint Tn) (fun CC : @Tpoint Tn => and (@Cong Tn A CC B CC) (and (@Cong Tn A CC C CC) (@Coplanar Tn A B C CC))) *)
        assumption.

(* Goal: and (@Cong Tn A CC C CC) (@Coplanar Tn A B C CC) *)
(* Goal: @ex (@Tpoint Tn) (fun CC : @Tpoint Tn => and (@Cong Tn A CC B CC) (and (@Cong Tn A CC C CC) (@Coplanar Tn A B C CC))) *)
      split.

(* Goal: @Cong Tn A CC C CC *)
(* Goal: @Coplanar Tn A B C CC *)
(* Goal: @ex (@Tpoint Tn) (fun CC : @Tpoint Tn => and (@Cong Tn A CC B CC) (and (@Cong Tn A CC C CC) (@Coplanar Tn A B C CC))) *)
        elim (eq_dec_points CC B1); intro HEq; try subst.

(* Goal: @Perp_at Tn I B1 B2 A C *)
(* Goal: @Coplanar Tn A B C CC *)
(* Goal: @ex (@Tpoint Tn) (fun CC : @Tpoint Tn => and (@Cong Tn A CC B CC) (and (@Cong Tn A CC C CC) (@Coplanar Tn A B C CC))) *)
          apply perp_bisect_cong_1 with B2; assumption.

(* Goal: @Cong Tn A CC C CC *)
(* Goal: @Coplanar Tn A B C CC *)
(* Goal: @ex (@Tpoint Tn) (fun CC : @Tpoint Tn => and (@Cong Tn A CC B CC) (and (@Cong Tn A CC C CC) (@Coplanar Tn A B C CC))) *)
          apply perp_bisect_cong_1 with B1.
(* Goal: @Perp_bisect Tn CC B1 A C *)
(* Goal: @Coplanar Tn A B C CC *)
(* Goal: @ex (@Tpoint Tn) (fun CC : @Tpoint Tn => and (@Cong Tn A CC B CC) (and (@Cong Tn A CC C CC) (@Coplanar Tn A B C CC))) *)
          apply perp_bisect_sym_1.
(* Goal: not (@eq (@Tpoint Tn) B1 B2) *)
(* Goal: not (@eq (@Tpoint Tn) C1 C2) *)
(* Goal: @Coplanar Tn B1 B2 C1 C2 *)
(* Goal: not (@ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X B1 B2) (@Col Tn X C1 C2))) *)
(* Goal: @Col Tn A B C *)
          apply perp_bisect_equiv_def in HAC.
(* Goal: not (@eq (@Tpoint Tn) B1 B2) *)
(* Goal: not (@eq (@Tpoint Tn) C1 C2) *)
(* Goal: @Coplanar Tn B1 B2 C1 C2 *)
(* Goal: not (@ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X B1 B2) (@Col Tn X C1 C2))) *)
(* Goal: @Col Tn A B C *)
          destruct HAC as [I [HPerp HMid]].
(* Goal: @Perp_bisect Tn B1 CC A C *)
(* Goal: @Coplanar Tn A B C CC *)
(* Goal: @ex (@Tpoint Tn) (fun CC : @Tpoint Tn => and (@Cong Tn A CC B CC) (and (@Cong Tn A CC C CC) (@Coplanar Tn A B C CC))) *)
          apply perp_bisect_equiv_def.
(* Goal: @Perp_bisect_bis Tn B1 CC A C *)
(* Goal: @Coplanar Tn A B C CC *)
(* Goal: @ex (@Tpoint Tn) (fun CC : @Tpoint Tn => and (@Cong Tn A CC B CC) (and (@Cong Tn A CC C CC) (@Coplanar Tn A B C CC))) *)
          exists I; split; try assumption.
(* Goal: @Perp_at Tn I A C B1 B2 *)
(* Goal: @Coplanar Tn A B C CC *)
(* Goal: @ex (@Tpoint Tn) (fun CC : @Tpoint Tn => and (@Cong Tn A CC B CC) (and (@Cong Tn A CC C CC) (@Coplanar Tn A B C CC))) *)
          apply perp_in_sym.
(* Goal: @Perp_at Tn I A C B1 CC *)
(* Goal: @Coplanar Tn A B C CC *)
(* Goal: @ex (@Tpoint Tn) (fun CC : @Tpoint Tn => and (@Cong Tn A CC B CC) (and (@Cong Tn A CC C CC) (@Coplanar Tn A B C CC))) *)
          apply perp_in_col_perp_in with B2; Col.
(* Goal: @Perp_at Tn I A C B1 B2 *)
(* Goal: @Coplanar Tn A B C CC *)
(* Goal: @ex (@Tpoint Tn) (fun CC : @Tpoint Tn => and (@Cong Tn A CC B CC) (and (@Cong Tn A CC C CC) (@Coplanar Tn A B C CC))) *)
          apply perp_in_sym.
(* Goal: @Perp_at Tn I B1 B2 A C *)
(* Goal: @Coplanar Tn A B C CC *)
(* Goal: @ex (@Tpoint Tn) (fun CC : @Tpoint Tn => and (@Cong Tn A CC B CC) (and (@Cong Tn A CC C CC) (@Coplanar Tn A B C CC))) *)
          assumption.

(* Goal: @Coplanar Tn A B C CC *)
(* Goal: @ex (@Tpoint Tn) (fun CC : @Tpoint Tn => and (@Cong Tn A CC B CC) (and (@Cong Tn A CC C CC) (@Coplanar Tn A B C CC))) *)
        destruct HCop1 as [HCop1 HCop3].
(* Goal: @Coplanar Tn A B C CC *)
(* Goal: @ex (@Tpoint Tn) (fun CC : @Tpoint Tn => and (@Cong Tn A CC B CC) (and (@Cong Tn A CC C CC) (@Coplanar Tn A B C CC))) *)
        destruct HAB as [[_ HE] HAB].
(* Goal: @Coplanar Tn A B C CC *)
(* Goal: @ex (@Tpoint Tn) (fun CC : @Tpoint Tn => and (@Cong Tn A CC B CC) (and (@Cong Tn A CC C CC) (@Coplanar Tn A B C CC))) *)
        elim HE; clear HE; intro; [assert_diffs|exfalso; auto].
(* Goal: @Coplanar Tn A B C CC *)
(* Goal: @ex (@Tpoint Tn) (fun CC : @Tpoint Tn => and (@Cong Tn A CC B CC) (and (@Cong Tn A CC C CC) (@Coplanar Tn A B C CC))) *)
        apply col_cop2__cop with C1 C2; Col; Cop.

(* Goal: @ex (@Tpoint Tn) (fun CC : @Tpoint Tn => and (@Cong Tn A CC B CC) (and (@Cong Tn A CC C CC) (@Coplanar Tn A B C CC))) *)
  exfalso; apply HNC.
(* Goal: @Col Tn A B C *)
  assert (HPar : Par B1 B2 C1 C2).

(* Goal: @Par Tn B1 B2 C1 C2 *)
(* Goal: @Col Tn A B C *)
    unfold Par; left.
(* Goal: and (@Cong Tn A CC C CC) (@Coplanar Tn A B C CC) *)
(* Goal: @ex (@Tpoint Tn) (fun CC : @Tpoint Tn => and (@Cong Tn A CC B CC) (and (@Cong Tn A CC C CC) (@Coplanar Tn A B C CC))) *)
    repeat split.

(* Goal: not (@eq (@Tpoint Tn) B1 B2) *)
(* Goal: not (@eq (@Tpoint Tn) C1 C2) *)
(* Goal: @Coplanar Tn B1 B2 C1 C2 *)
(* Goal: not (@ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X B1 B2) (@Col Tn X C1 C2))) *)
(* Goal: @Col Tn A B C *)
      apply perp_bisect_equiv_def in HAC.
(* Goal: not (@eq (@Tpoint Tn) B1 B2) *)
(* Goal: not (@eq (@Tpoint Tn) C1 C2) *)
(* Goal: @Coplanar Tn B1 B2 C1 C2 *)
(* Goal: not (@ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X B1 B2) (@Col Tn X C1 C2))) *)
(* Goal: @Col Tn A B C *)
      destruct HAC as [I [HPerp HMid]].
(* Goal: not (@eq (@Tpoint Tn) C1 C2) *)
(* Goal: @Coplanar Tn B1 B2 C1 C2 *)
(* Goal: not (@ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X B1 B2) (@Col Tn X C1 C2))) *)
(* Goal: @Col Tn A B C *)
      apply perp_in_distinct in HPerp.
(* Goal: @Perp_at Tn I B1 B2 A C *)
(* Goal: @Coplanar Tn A B C CC *)
(* Goal: @ex (@Tpoint Tn) (fun CC : @Tpoint Tn => and (@Cong Tn A CC B CC) (and (@Cong Tn A CC C CC) (@Coplanar Tn A B C CC))) *)
      spliter; assumption.

(* Goal: not (@eq (@Tpoint Tn) C1 C2) *)
(* Goal: @Coplanar Tn B1 B2 C1 C2 *)
(* Goal: not (@ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X B1 B2) (@Col Tn X C1 C2))) *)
(* Goal: @Col Tn A B C *)
      apply perp_bisect_equiv_def in HAB.
(* Goal: not (@eq (@Tpoint Tn) C1 C2) *)
(* Goal: @Coplanar Tn B1 B2 C1 C2 *)
(* Goal: not (@ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X B1 B2) (@Col Tn X C1 C2))) *)
(* Goal: @Col Tn A B C *)
      destruct HAB as [I [HPerp HMid]].
(* Goal: not (@eq (@Tpoint Tn) C1 C2) *)
(* Goal: @Coplanar Tn B1 B2 C1 C2 *)
(* Goal: not (@ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X B1 B2) (@Col Tn X C1 C2))) *)
(* Goal: @Col Tn A B C *)
      apply perp_in_distinct in HPerp.
(* Goal: @Perp_at Tn I B1 B2 A C *)
(* Goal: @Coplanar Tn A B C CC *)
(* Goal: @ex (@Tpoint Tn) (fun CC : @Tpoint Tn => and (@Cong Tn A CC B CC) (and (@Cong Tn A CC C CC) (@Coplanar Tn A B C CC))) *)
      spliter; assumption.

(* Goal: @Coplanar Tn B1 B2 C1 C2 *)
(* Goal: not (@ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X B1 B2) (@Col Tn X C1 C2))) *)
(* Goal: @Col Tn A B C *)
      spliter; CopR.

(* Goal: not (@ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X B1 B2) (@Col Tn X C1 C2))) *)
(* Goal: @Col Tn A B C *)
      intro HInter'; apply HInter.
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I B1 B2) (@Col Tn I C1 C2)) *)
(* Goal: @Col Tn A B C *)
      destruct HInter' as [I HInter'].
(* Goal: @Perp_at Tn I B1 B2 A C *)
(* Goal: @Coplanar Tn A B C CC *)
(* Goal: @ex (@Tpoint Tn) (fun CC : @Tpoint Tn => and (@Cong Tn A CC B CC) (and (@Cong Tn A CC C CC) (@Coplanar Tn A B C CC))) *)
      exists I; assumption.

(* Goal: @Col Tn A B C *)
  clear HInter.
(* Goal: @Col Tn A B C *)
  apply perp_bisect_perp in HAB; apply perp_bisect_perp in HAC.
(* Goal: @Col Tn A B C *)
  assert (HPerp := HPTP B1 B2 C1 C2 A C HPar HAC).
(* Goal: @Col Tn A B C *)
  apply par_id.
(* Goal: @Par Tn A B A C *)
  spliter.
(* Goal: @Par Tn A B A C *)
  apply l12_9 with C1 C2; Perp; Cop; try CopR.
(* Goal: @Perp Tn A C C1 C2 *)
  apply perp_sym, HPerp; CopR.
Qed.

End par_perp_perp_TCP.