Library GeoCoq.Meta_theory.Parallel_postulates.par_perp_perp_TCP

Require Export GeoCoq.Meta_theory.Parallel_postulates.Euclid_def.

Section par_perp_perp_TCP.

Context `{MT:Tarski_2D}.

Lemma par_perp_perp_implies_perp_bisect_existence :
  perpendicular_transversal_postulate
   A B, A B P, Q, Perp_bisect P Q A B.
Proof.
intros HPTP A B HDiff.
assert (HM := midpoint_existence A B); destruct HM as [M HM].
assert(HP' := l6_25 A B HDiff); destruct HP' as [P' HP'].
assert(HQ' := l8_18_existence A B P' HP'); clear HP'.
destruct HQ' as [Q' [Hc HP'Q']]; clear Hc.
assert (HPQ := parallel_existence P' Q' M).
destruct HPQ as [P [Q [HDiff' [HPar HCol]]]]; try (assert_diffs; assumption).
P; Q; unfold Perp_bisect.
split; assert_diffs; Col.
split; try ( M; split; Col; Midpoint); left.
apply HPTP with P' Q'; finish.
Qed.

Lemma inter_dec_plus_par_perp_perp_imply_triangle_circumscription :
  decidability_of_intersection
  perpendicular_transversal_postulate
  triangle_circumscription_principle.
Proof.
intros HID HPTP A B C HNC.
assert (HAB := par_perp_perp_implies_perp_bisect_existence HPTP A B);
destruct HAB as [C1 [C2 HAB]]; try (assert_diffs; assumption).
assert (HAC := par_perp_perp_implies_perp_bisect_existence HPTP A C);
destruct HAC as [B1 [B2 HAC]]; try (assert_diffs; assumption).
assert (HInter := HID B1 B2 C1 C2).
elim HInter; clear HInter; intro HInter.

  destruct HInter as [CC [HCol1 HCol2]].

     CC; split.

      elim (eq_dec_points CC C1); intro HEq; try subst.

        apply perp_bisect_cong_1 with C2; assumption.

        apply perp_bisect_cong_1 with C1.
        apply perp_bisect_sym_1.
        apply perp_bisect_equiv_def in HAB.
        destruct HAB as [I [HPerp HMid]].
        apply perp_bisect_equiv_def.
         I; split; try assumption.
        apply perp_in_sym.
        apply perp_in_col_perp_in with C2; Col.
        apply perp_in_sym.
        assumption.

      elim (eq_dec_points CC B1); intro HEq; try subst.

        apply perp_bisect_cong_1 with B2; assumption.

        apply perp_bisect_cong_1 with B1.
        apply perp_bisect_sym_1.
        apply perp_bisect_equiv_def in HAC.
        destruct HAC as [I [HPerp HMid]].
        apply perp_bisect_equiv_def.
         I; split; try assumption.
        apply perp_in_sym.
        apply perp_in_col_perp_in with B2; Col.
        apply perp_in_sym.
        assumption.

  exfalso; apply HNC.
  assert (HPar : Par B1 B2 C1 C2).

    unfold Par; left.
    repeat split.

      apply perp_bisect_equiv_def in HAC.
      destruct HAC as [I [HPerp HMid]].
      apply perp_in_distinct in HPerp.
      spliter; assumption.

      apply perp_bisect_equiv_def in HAB.
      destruct HAB as [I [HPerp HMid]].
      apply perp_in_distinct in HPerp.
      spliter; assumption.

      apply all_coplanar.

      intro HInter'; apply HInter.
      destruct HInter' as [I HInter'].
       I; assumption.

  clear HInter; clear HNC.
  apply perp_bisect_perp in HAB; apply perp_bisect_perp in HAC.
  assert (HPerp := HPTP B1 B2 C1 C2 A C HPar HAC).
  apply par_id.
  apply l12_9 with C1 C2; finish.
Qed.

End par_perp_perp_TCP.