proposition: Lemma two_sides_not_col : forall A B X Y, TS A B X Y -> ~ Col A B X.
proof: Proof. intros. unfold TS in H. spliter. intro. apply H. apply col_permutation_2. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar