proposition: Lemma col_one_side : forall A B C P Q, Col A B C -> A <> C -> OS A B P Q -> OS A C P Q.
proof: Proof. unfold OS. intros. ex_and H1 T. exists T. split; eapply (col_two_sides _ B); assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar