proposition: Lemma triangle_circumscription_implies_tarski_s_euclid_aux1 : forall A B C D T X Y Z M1 Z1, triangle_circumscription_principle -> B <> D -> C <> D -> D <> T -> T <> X -> ~ Col A B C -> Col A B M1 -> Bet A D T -> ~ Col B C T -> Bet B D C -> Col T Y Z -> Bet Y T X -> Bet Y M1 Z1 -> Cong Y T T X -> Cong Y M1 M1 Z1 -> Perp B C T Z -> Perp A B Y Z1 -> exists x, Col A B x /\ Par_strict B C x T /\ Cong X x Y x.
proof: Proof. intros A B C D T X Y Z M1 Z1; intro HTC. intros HBD HCD HDT HTX. intros HABC HABM1 HADT HBCT HBDC HTYZ HYTX HYM1Z1. intros HCong1 HCong2 HPerp1 HPerp2. assert (A <> D) by (intro; subst; apply HABC; Col). assert_diffs. assert (HCopA : Coplanar B C T A) by (exists D; left; split; Col). assert (HCopB : Coplanar B C T B) by Cop. assert (HCopC : Coplanar B C T C) by Cop. assert (HCopT : Coplanar B C T T) by Cop. assert (HCopZ : Coplanar B C T Z) by Cop. assert (HCopY : Coplanar B C T Y) by (apply col_cop__cop with Z; Col). assert (HCopX : Coplanar B C T X) by (apply col_cop__cop with Y; Col). assert (HXYZ1 : ~ Col X Y Z1). { intro; apply HABC, col_permutation_4, par_id. assert (Col T Z Z1) by ColR. assert (Coplanar B C Y Z1) by (apply col2_cop__cop with T Z; Col). apply l12_9 with Y Z1; [Cop..| |Perp|]. apply coplanar_pseudo_trans with B C T; auto; apply col_cop__cop with Z; auto. apply perp_sym, perp_col2 with T Z; Perp; Col. } destruct (HTC X Y Z1 HXYZ1) as [x [HCong3 [HCong4 HCop1]]]; exists x. assert (HYM1 : Y <> M1) by (intro; treat_equalities; auto). assert (HCopZ1 : Coplanar B C T Z1). { assert (~ Col A B Y) by (intro; destruct (perp_not_col2 A B Y Z1) as [|HNCol]; Perp; apply HNCol; ColR). apply coplanar_pseudo_trans with A B Y; [| |apply coplanar_pseudo_trans with B C T..|]; Cop. } assert (HCopx : Coplanar B C T x). apply coplanar_pseudo_trans with X Y Z1; trivial; apply coplanar_pseudo_trans with B C T; assumption. assert (Col A B x). { apply cong_cop2_perp_bisect_col with Y Z1; trivial. apply coplanar_pseudo_trans with B C T; assumption. apply coplanar_pseudo_trans with B C T; assumption. apply cong_transitivity with X x; Cong. repeat split; Perp. exists M1; repeat split; Between; Cong. } do 2 (split; trivial). apply par_not_col_strict with T; Col. apply l12_9 with X Y; [apply coplanar_pseudo_trans with B C T; assumption..| |]. apply perp_sym, perp_col2 with T Z; Perp; ColR. apply perp_bisect_perp; apply cong_cop_perp_bisect; Cong; [|Cop]. intro; subst; apply HABC; ColR. 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