proposition: Lemma impossible_case_4_2 : forall A B C D T x y, ~ Col A B C -> Col A C y -> Bet A D T -> ~ Col B C T -> Bet B D C -> Bet B A x -> Bet T y x -> Par_strict B C x y -> False.
proof: Proof. intros A B C D T x y. intros HABC HACy HADT HBCT HBDC HABx HTyx HPar. assert (HTS : TS B C A T) by (repeat split; [..|exists D; split]; Col). assert (HOS : OS B C A x). { assert (HBCB : Col B C B) by Col. assert (HABx' : Col A x B) by Col. assert (H := l9_19 B C A x B HBCB HABx'); rewrite H. apply not_col_distincts in HABC; spliter. split; [Out|Col]. } assert (HTS' : TS B C x T) by (apply l9_8_2 with A; assumption); clear HTS; clear HOS; destruct HTS' as [_ [_ [I [HBCI HITx]]]]. assert (HTx : T <> x) by (intro; treat_equalities; apply HBCT; Col). assert (HPar' : Par_strict B C x T) by (apply par_strict_col_par_strict with y; Col). apply HPar'; exists I; 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