proposition: Lemma triangle_circumscription_implies_tarski_s_euclid : triangle_circumscription_principle -> tarski_s_parallel_postulate.
proof: Proof. unfold tarski_s_parallel_postulate. intro HTC; apply tarski_s_euclid_remove_degenerated_cases. intros A B C D T HAB HAC HAD HAT HBC HBD HBT HCD HCT HDT HABC HADT HBDC HBCT. clear HAT HBT HCT. assert (HY := l8_18_existence B C T HBCT); destruct HY as [Y [HBCY HPerp]]. revert B C HAB HAC HBC HBD HCD HABC HBDC HBCT HBCY HPerp. cut (forall B C, A <> B -> A <> C -> B <> C -> B <> D -> C <> D -> ~ Col A B C -> Bet B D C -> ~ Col B C T -> Col B C Y -> Perp B C T Y -> B <> Y -> exists x y : Tpoint, Bet A B x /\ Bet A C y /\ Bet x T y). { intros Haux B C HAB HAC HBC HBD HCD HABC HBDC HBCT HBCY HPerp. elim (eq_dec_points B Y); auto. intro HBY. elim (eq_dec_points C Y); intro HCY. subst; exfalso; apply HBC; reflexivity. apply between_symmetry in HBDC. apply perp_left_comm in HPerp. destruct (Haux C B) as [y [x [HACy [HABx HxTy]]]]; Col. exists x, y; repeat split; Between. } intros B C HAB HAC HBC HBD HCD HABC HBDC HBCT HBCY HPerp HBY. elim (eq_dec_points C Y); intro HCY. { treat_equalities. assert (HCT : C <> T) by (apply not_col_distincts in HBCT; spliter; auto). assert (HY := midpoint_existence C T); destruct HY as [Y HY]. assert (HAY : A <> Y) by (intro; treat_equalities; apply HABC; ColR). assert (H := midpoint_distinct_1 Y C T HCT HY); destruct H as [HCY HTY]; apply not_eq_sym in HCY; apply not_eq_sym in HTY. assert (HBY : B <> Y) by (intro; subst; apply HBCT; Col). destruct HY as [HCTY HCYTY]. assert (HACY : ~ Col A B Y) by (apply impossible_two_sides_not_col with C D T; Between; Col). assert (HX := symmetric_point_construction Y T); destruct HX as [X HX]. assert (H := midpoint_distinct_2 T Y X HTY HX); destruct H as [HTX HXY]; apply not_eq_sym in HTX. destruct HX as [HXTY HXTYT]. assert (HZ1 := l10_2_existence A B Y); destruct HZ1 as [Z1 HZ1]. elim HZ1; clear HZ1; intro HZ1; destruct HZ1 as [Hclear HZ1]; [|contradiction]; clear Hclear. destruct HZ1 as [[M1 [[HXM1Z1 HM1XM1Z1] HABM1]] HZ1]. assert (HZ2 := l10_2_existence A C Y); destruct HZ2 as [Z2 HZ2]. elim HZ2; clear HZ2; intro HZ2; destruct HZ2 as [Hclear HZ2]; [|contradiction]; clear Hclear. destruct HZ2 as [[M2 [[HXM2Z2 HM2XM2Z2] HACM2]] HZ2]. elim HZ2; clear HZ2; intro HZ2; [|treat_equalities; exfalso; apply HABC; ColR]. elim HZ1; clear HZ1; intro HZ1; [|treat_equalities; contradiction]. apply triangle_circumscription_implies_tarski_s_euclid_aux with D X Y C M1 Z1 M2 Z2; Col. } { assert (HX := symmetric_point_construction Y T); destruct HX as [X HX]. assert (H := perp_distinct B C T Y HPerp); destruct H as [Hclear HTY]; clear Hclear. assert (H := midpoint_distinct_2 T Y X HTY HX); destruct H as [HTX HXY]; apply not_eq_sym in HTX. destruct HX as [HXTY HXTYT]. assert (HZ1 := l10_2_existence A B Y); destruct HZ1 as [Z1 HZ1]. elim HZ1; clear HZ1; intro HZ1; destruct HZ1 as [Hclear HZ1]; [|contradiction]; clear Hclear. destruct HZ1 as [[M1 [[HXM1Z1 HM1XM1Z1] HABM1]] HZ1]. assert (HZ2 := l10_2_existence A C Y); destruct HZ2 as [Z2 HZ2]. elim HZ2; clear HZ2; intro HZ2; destruct HZ2 as [Hclear HZ2]; [|contradiction]; clear Hclear. destruct HZ2 as [[M2 [[HXM2Z2 HM2XM2Z2] HACM2]] HZ2]. assert (HABY : ~ Col A B Y) . (intro; apply HBY; apply l6_21 with A B C B; Col). assert (HACY : ~ Col A C Y) by (intro; apply HCY; apply l6_21 with A C B C; Col). elim HZ1; clear HZ1; intro HZ1; [|treat_equalities; contradiction]. elim HZ2; clear HZ2; intro HZ2; [|treat_equalities; contradiction]. apply triangle_circumscription_implies_tarski_s_euclid_aux with D X Y Y M1 Z1 M2 Z2; Col. } 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