proposition: Lemma one_side_not_col124 : forall A B X Y, OS A B X Y -> ~ Col A B Y.
proof: Proof. intros A B X Y HOS. apply one_side_not_col123 with X. apply one_side_symmetry, HOS. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar