proposition: Lemma ts__ncol : forall A B X Y, TS A B X Y -> ~Col A X Y \/ ~Col B X Y.
proof: Proof. intros. unfold TS in H. spliter. ex_and H1 T. assert(X <> Y). intro. treat_equalities. contradiction. induction(eq_dec_points A T). treat_equalities. right. intro. apply H. ColR. left. intro. apply H. ColR. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar