proposition: Lemma cong2__ncol : forall P A B C, A <> B -> B <> C -> A <> C -> Cong A P B P -> Cong A P C P -> ~ Col A B C.
proof: Proof. assert (H : forall P A B C, A <> B -> B <> C -> Cong A P C P -> Cong B P C P -> ~ Bet A B C). { intros P A B C HAB HBC HCong1 HCong2 HBet. apply (bet_le__lt A C P B); Le. } intros P A B C; intros. assert (Cong B P C P) by (apply cong_transitivity with A P; Cong). intro HCol; elim HCol; [|intro Hd; elim Hd]; apply (H P); Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2