proposition: Lemma triangle_circumscription_implies_tarski_s_euclid_aux : forall A B C D T X Y Z M1 Z1 M2 Z2, triangle_circumscription_principle -> B <> D -> C <> D -> D <> T -> T <> X -> ~ Col A B C -> Col A B M1 -> Col A C M2 -> Bet A D T -> ~ Col B C T -> Bet B D C -> Col T Y Z -> Bet Y T X -> Bet Y M1 Z1 -> Bet Y M2 Z2 -> Cong Y T T X -> Cong Y M1 M1 Z1 -> Cong Y M2 M2 Z2 -> Perp B C T Z -> Perp A B Y Z1 -> Perp A C Y Z2 -> exists x, exists y, Bet A B x /\ Bet A C y /\ Bet x T y.
proof: Proof. intros A B C D T X Y Z M1 Z1 M2 Z2; intro HTC. intros HBD HCD HDT HTX. intros HABC HABM1 HACM2 HADT HBCT HBDC HTYZ HYTX HYM1Z1. intros HYM2Z2 HCong5 HCong6 HCong7 HPerp1 HPerp2 HPerp3. assert (Hx := triangle_circumscription_implies_tarski_s_euclid_aux1 A B C D T X Y Z M1 Z1). destruct Hx as [x [HABx [Hx1 Hx2]]]; [assumption..|]; exists x. assert (Hy := triangle_circumscription_implies_tarski_s_euclid_aux1 A C B D T X Y Z M2 Z2). destruct Hy as [y [HACy [Hy1 Hy2]]]; [Between; Col; Perp..|]; exists y. assert (HxTy : Col x T y). { elim (eq_dec_points T x); intro; [|elim (eq_dec_points T y); intro]; [subst; Col..|]. assert_diffs. apply col_permutation_4, cop_perp2__col with X Y; [|apply perp_bisect_perp, cong_cop_perp_bisect; Cong; Cop..]. assert (Coplanar B C T Y) by (apply col_cop__cop with Z; Col; Cop). assert (Coplanar B C T X) by (apply col_cop__cop with Y; Col). apply coplanar_pseudo_trans with B C T; Cop. } assert (HPar : Par_strict B C x y). { apply par_strict_col_par_strict with T; Col. intro; subst y. destruct HPerp3 as [_ [HAC _]]. assert (A = x) by (apply (l6_21 A B C A); Col). subst; apply Hx1; exists D; split; Col. } assert (A <> D) by (intro; subst; apply HABC; Col). elim HxTy; clear HxTy; intro HxTy. elim HABx; clear HABx; intro HABx. elim HACy; clear HACy; intro HACy; auto. exfalso; elim HACy; clear HACy; intro HACy. apply (impossible_case_1 A B C x y); assumption. apply (impossible_case_2 A B C D T x y); Col. exfalso; elim HABx; clear HABx; intro HABx. apply (impossible_case_3 A B C D T x y); assumption. apply (impossible_case_2 A C B D T y x); Col; Between. exfalso; elim HxTy; clear HxTy; intro HxTy. apply (impossible_case_4 A B C D T x y); assumption. apply (impossible_case_4 A C B D T y x); Between; Col; Par. Qed.
imports: GeoCoq.Axioms.parallel_postulates GeoCoq.Meta_theory.Parallel_postulates.tarski_s_euclid_remove_degenerated_cases GeoCoq.Tarski_dev.Annexes.perp_bisect GeoCoq.Tarski_dev.Ch12_parallel