proposition: Lemma impossible_case_8 : forall P Q R S U I, BetS Q U R -> ~ Col P Q S -> Par P R Q S -> Par P S Q R -> Col P U I -> Bet I S Q -> False.
proof: Proof. intros P Q R S U I HQUR HNC HPar1 HPar2 HPUI HSQI. apply BetSEq in HQUR. destruct HQUR as [HQUR [HQU [HQR HUR]]]. assert (H : Par_strict P S Q U) by (apply par_strict_col_par_strict with R; Col; apply par_not_col_strict with Q; Col; Par). apply between_symmetry in HSQI. elim HPUI; clear HPUI; intro HPUI. { apply H. destruct (inner_pasch P Q I U S HPUI HSQI) as [J [HQJU HPJS]]; exists J. split; Col. } { elim HPUI; clear HPUI; intro HPUI. { apply H. destruct (outer_pasch U Q I P S HPUI HSQI) as [J [HQJU HPSJ]]; exists J. split; Col. } { assert (H1 : Par_strict P R Q I). assert_diffs; apply par_strict_col_par_strict with S; Col. apply par_strict_symmetry, par_not_col_strict with P; Col; Par. apply H1. destruct (outer_pasch Q I U R P HQUR HPUI) as [J [HQJI HRPJ]]; exists J. split; Col. } } Qed.
imports: GeoCoq.Axioms.parallel_postulates GeoCoq.Meta_theory.Parallel_postulates.tarski_s_euclid_remove_degenerated_cases GeoCoq.Tarski_dev.Ch12_parallel