proposition: Lemma impossible_two_sides_not_col : forall A B C D T 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 Y T -> ~ Col A C Y.
proof: Proof. intros A B C D T Y HAD HBD HCD HDT. intros HABC HADT HBCT HBDC HBYT. apply one_side_not_col124 with B. apply l9_17 with T; trivial. assert (HOS : OS A C B D). apply invert_one_side, out_one_side; [Col|Out]. apply one_side_transitivity with D; trivial. 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