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