proposition: Lemma col124__nos : forall A B P Q, Col P Q B -> ~ OS P Q A B.
proof: Proof. intros A B P Q HCol. intro HOne. assert (HN : ~ OS P Q B A) by (apply col123__nos; auto). apply HN; apply one_side_symmetry; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar