proposition: Lemma impossible_case_4_1 : forall A B C D T x y, A <> D -> C <> D -> ~ Col A B C -> Col A C y -> Bet A D T -> ~ Col B C T -> Bet B D C -> Out A B x -> Bet T y x -> False.
proof: Proof. intros A B C D T x y. intros HAD HCD. intros HABC HACy HADT HBCT HBDC HABx HTyx. revert HACy. apply one_side_not_col124 with T. apply l9_17 with x; trivial. assert (HOS : OS A C B D) by (apply invert_one_side, out_one_side; [Col|Out]). apply one_side_transitivity with D. apply one_side_not_col124 in HOS; apply out_one_side; Out. apply one_side_transitivity with B; [Side|]. assert (HACA : Col A C A) by Col. assert (HABx' : Col B x A) by Col. assert (H := l9_19 A C B x A HACA HABx'); rewrite H. split; Col. Qed.
imports: GeoCoq.Axioms.parallel_postulates GeoCoq.Meta_theory.Parallel_postulates.tarski_s_euclid_remove_degenerated_cases GeoCoq.Tarski_dev.Annexes.perp_bisect GeoCoq.Tarski_dev.Ch12_parallel