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