proposition: Lemma strong_parallel_postulate_implies_tarski_s_euclid_aux : strong_parallel_postulate -> (forall A B D T, A <> B -> A <> D -> A <> T -> B <> D -> B <> T -> D <> T -> ~ Col A B T -> Bet A D T -> exists B', exists B'', exists MB, exists X, Bet A B X /\ Par_strict T X B D /\ BetS B MB T /\ BetS B' MB B'' /\ Cong B MB T MB /\ Cong B' MB B'' MB /\ Col B B' D /\ Bet B'' T X /\ B <> B' /\ B'' <> T).
proof: Proof. intros HSPP A B D T HAB HAD HAT HBD HBT HDT HABT HADT. destruct (symmetric_point_construction D B) as [B' HB']. destruct (midpoint_distinct_2 B D B' HBD HB') as [HB'D HBB']. destruct HB' as [HBDB' HCong1]. apply between_symmetry in HADT. apply between_symmetry in HBDB'. destruct (midpoint_existence B T) as [MB HMB]. destruct (midpoint_distinct_1 MB B T HBT HMB) as [HBMB HMBT]. destruct HMB as [HBMBT HCong2]. destruct (symmetric_point_construction B' MB) as [B'' HB'']. assert (HB'MB : MB <> B'). { intro; treat_equalities; apply HABT; ColR. } destruct (midpoint_distinct_2 MB B' B'' HB'MB HB'') as [HB'B'' HB''MB]. destruct HB'' as [HB'MBB'' HCong3]. assert (H1 : ~ Col B T B'') by (intro; apply HABT; ColR). assert (H2 : BetS B MB T) by (repeat split; Between). assert (H3 : BetS B' MB B'') by (repeat split; Between). destruct (outer_pasch T B' D A B HADT HBDB') as [B''' [HTB'''B' HABB''']]. assert (HB'B''' : B' <> B'''). { intro; treat_equalities; apply HABT; ColR. } assert (HB'''T : B''' <> T). { intro; treat_equalities; Col. } assert (H4 : BetS T B''' B') by (repeat split; Between). assert (HNC : ~ Col B B' B''') by (intro; apply H1; ColR). destruct (HSPP B T B' B'' MB B''') as [X [HBetS HX]]; Cong; [Cop|]. assert (HPar1 : Par B B' T B'') by (unfold BetS in *; spliter; apply l12_17 with MB; [|split..]; auto). assert (HPar2 : Par B B'' T B'). { apply not_col_distincts in H1; spliter. unfold BetS in *; spliter; apply l12_17 with MB; [|split..]; Between; Cong. } elim HBetS; clear HBetS; intro HBetS. { elim HX; clear HX; intro HX. { assert (H : BetS B'' T X). { repeat split; [|intro; treat_equalities..]; Col. apply HABT; ColR. } clear HBetS; rename H into HBetS. assert (H : BetS B B''' X). { repeat split; [|intro; treat_equalities..]; Col. unfold BetS in *; spliter; apply H1; ColR. } clear HX; rename H into HX. apply BetSEq in HBetS; destruct HBetS as [HB''TX [HB''T [HB''X HBTX]]]. exists B', B'', MB, X. split. unfold BetS in HX; spliter; eBetween. split. apply par_strict_col_par_strict with B'; Col. apply par_strict_symmetry, par_strict_col_par_strict with B''; Col. apply par_strict_symmetry, par_not_col_strict with B; Par; Col. repeat (split; [try assumption|]); Cong; Col. } { exfalso. elim HX; clear HX; intro HX. { apply (impossible_case_5 B T B' B'' B''' X); assumption. } { apply (impossible_case_6 B T B' B'' B''' X); assumption. } } } { exfalso. elim HBetS; clear HBetS; intro HBetS. { apply (impossible_case_7 B T B' B'' B''' X); assumption. } { apply (impossible_case_8 B T B' B'' B''' X); assumption. } } Qed.
imports: GeoCoq.Axioms.parallel_postulates GeoCoq.Meta_theory.Parallel_postulates.tarski_s_euclid_remove_degenerated_cases GeoCoq.Tarski_dev.Ch12_parallel