proposition: Lemma diff_col_ex : forall A B, exists C, A <> C /\ B <> C /\ Col A B C.
proof: Proof. intros. assert (exists C, Bet A B C /\ B <> C). apply point_construction_different. ex_and H C. exists C. split. intro. induction (eq_dec_points A B). subst B. subst C. intuition. treat_equalities. auto. assert_cols. auto. Qed.
imports: GeoCoq.Tarski_dev.Ch05_bet_le