proposition: Lemma impossible_case_2 : forall A B C D T x y, A <> D -> B <> D -> C <> D -> D <> T -> ~ Col A B C -> Col A B x -> Bet A D T -> ~ Col B C T -> Bet B D C -> Bet y A C -> Bet x T y -> False.
proof: Proof. intros A B C D T x y. intros HAD HBD HCD HDT. intros HABC HABx HADT HBCT HBDC HACy HxTy. assert (HAy : A <> y) by (intro; apply HBCT; ColR). revert HABx. apply one_side_not_col124 with T. apply bet_ts__os with y; Between. apply l9_2, l9_8_2 with C. apply bet__ts; Between. assert (HOS : OS A B C D) by (apply invert_one_side, out_one_side; [Col|Out]). apply one_side_transitivity with D; Side. apply one_side_not_col124 in HOS. apply out_one_side; 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