proposition: Lemma impossible_case_6 : forall P Q R S U I, BetS Q U R -> ~ Col P Q S -> Par P S Q R -> Bet S Q I -> Bet I P U -> False.
proof: Proof. intros P Q R S U I HQUR HNC HPar HSQI HPUI. apply BetSEq in HQUR. apply between_symmetry in HPUI. destruct (inner_pasch S U I Q P HSQI HPUI) as [J [HBet1 HBet2]]. assert (HParS : Par_strict P S Q U). { spliter. apply par_strict_col_par_strict with R; Col. apply par_not_col_strict with Q; Col. } apply HParS; 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