proposition: Lemma strong_parallel_postulate_implies_tarski_s_euclid : strong_parallel_postulate -> tarski_s_parallel_postulate.
proof: Proof. unfold tarski_s_parallel_postulate. intro HSPP; 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. assert (~ Col A B T) by (intro; apply HABC; ColR). assert (~ Col A C T) by (intro; apply HABC; ColR). destruct (strong_parallel_postulate_implies_tarski_s_euclid_aux HSPP A B D T) as [B' [B'' [MB [X [HABX [HPar' [HBet1 [HBet2 [HCong1 [HCong2 [HBB'D [HB''TX [HBB' HB''T]]]]]]]]]]]]]; [assumption..|]. destruct (strong_parallel_postulate_implies_tarski_s_euclid_aux HSPP A C D T) as [_ [_ [_ [Y [HACY [HPar _]]]]]]; Between. exists X; exists Y; repeat (split; [assumption|]). elim (col_dec X T Y); intro HXTY. { clear dependent MB; clear dependent B'; clear dependent B''. assert (HAXY : ~ Col A X Y) by (intro; apply HABC; ColR). apply between_symmetry in HACY. assert (HU := outer_pasch Y B C A D HACY HBDC); destruct HU as [U [HYUB HADU]]. apply between_symmetry in HABX. assert (HV := outer_pasch X Y B A U HABX HYUB); destruct HV as [V [HXVY HAUV]]. assert (HEq : T = V) by (apply (l6_21 X Y A D); ColR). subst; assumption. } { clear dependent A. assert (HNC : ~ Col T B'' Y) by (intro; apply HXTY; ColR). apply (par_strict_col_par_strict T Y C D B) in HPar; Col. apply (par_strict_col_par_strict T X B D C) in HPar'; Col. assert (HCop : Coplanar T B B'' Y). { apply not_col_distincts in HXTY; spliter. apply coplanar_perm_13, col_cop__cop with X; Col. apply coplanar_perm_4, coplanar_trans_1 with C; Col; Cop. } unfold BetS in *; spliter. destruct (HSPP T B B'' B' MB Y) as [I [HCol1 HCol2]]; Cong; [repeat split; Between..|]. exfalso; apply HPar; exists I; split; ColR. } Qed.
imports: GeoCoq.Axioms.parallel_postulates GeoCoq.Meta_theory.Parallel_postulates.tarski_s_euclid_remove_degenerated_cases GeoCoq.Tarski_dev.Ch12_parallel