proposition: Lemma impossible_case_7 : forall P Q R S U I, BetS Q U R -> ~ Col P Q S -> ~ Col P R U -> Par P R Q S -> Par P S Q R -> Col P U I -> Bet Q I S -> False.
proof: Proof. intros P Q R S U I HQUR HNC HNC' HPar1 HPar2 HPUI HSQI. apply BetSEq in HQUR. revert HPUI. apply one_side_not_col124 with Q. apply l9_17 with S; [|assumption]. destruct HQUR as [HQUR HDiff]. apply between_symmetry in HQUR. exists R; split. spliter; apply l9_2, invert_two_sides, bet__ts; Col. apply l9_31. { apply one_side_symmetry, l9_17 with Q; [|assumption]. apply l12_6, par_not_col_strict with Q; Par; Col. } apply one_side_transitivity with Q. spliter; apply invert_one_side, out_one_side; [Col|Out]. apply l12_6, par_strict_symmetry, par_not_col_strict with P; Par; Col. Qed.
imports: GeoCoq.Axioms.parallel_postulates GeoCoq.Meta_theory.Parallel_postulates.tarski_s_euclid_remove_degenerated_cases GeoCoq.Tarski_dev.Ch12_parallel