proposition: Lemma impossible_case_4 : forall A B C D T x y, A <> D -> B <> D -> C <> D -> D <> T -> ~ Col A B C -> Col A C y -> Bet A D T -> ~ Col B C T -> Bet B D C -> Col A B x -> Bet T y x -> Par_strict B C x y -> False.
proof: Proof. intros A B C D T x y. intros HAD HBD HCD HDT. intros HABC HACy HADT HBCT HBDC HABx HTyx HPar. revert HABx. destruct (or_bet_out B A x) as [HABx|[HABx|HABx]]; [intro..|Col]. apply (impossible_case_4_2 A B C D T x y); auto. apply (impossible_case_4_1 A B C D T x y); auto. 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