proposition: Lemma impossible_case_3 : forall A B C D T x y, A <> D -> B <> D -> C <> D -> D <> T -> ~ Col A B C -> Bet A D T -> ~ Col B C T -> Bet B D C -> Bet B x A -> Bet x T y -> Par_strict B C x y -> False.
proof: Proof. intros A B C D T x y. intros HAD HBD HCD HDT. intros HABC HADT HBCT HBDC HABx HxTy HPar. apply l12_6 in HPar. absurd (TS B C x y); Side. apply bet_ts__ts with T; trivial. apply l9_8_2 with A. repeat split; Col; exists D; split; Col. assert_diffs; apply out_one_side; [Col|Out]. 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