proposition: Lemma impossible_case_5 : forall P Q R S U I, BetS Q U R -> ~ Col P Q S -> ~ Col P R U -> Par P R Q S -> Bet S Q I -> Bet U I P -> False.
proof: Proof. intros P Q R S U I HQUR HNC HNC' HPar HSQI HPUI. apply BetSEq in HQUR. apply par_symmetry in HPar. apply (par_not_col_strict Q S P R P) in HPar; Col. assert (HOS : OS Q S R U). { assert (HQS : Q <> S) by (assert_diffs; auto). assert (HQSQ : Col Q S Q) by Col. assert (HRUQ : Col R U Q) by (spliter; Col). rewrite (l9_19 Q S R U Q HQSQ HRUQ). spliter. split; [Out|apply par_strict_not_col_4 with P, HPar]. } apply (l9_9 Q S P U); [|apply one_side_transitivity with R; Side]. apply one_side_not_col124 in HOS. spliter; repeat split; Col. exists I; split; [Col|Between]. Qed.
imports: GeoCoq.Axioms.parallel_postulates GeoCoq.Meta_theory.Parallel_postulates.tarski_s_euclid_remove_degenerated_cases GeoCoq.Tarski_dev.Ch12_parallel