proposition: Lemma osp_symmetry : forall A B C P Q, OSP A B C P Q -> OSP A B C Q P.
proof: Proof. intros A B C P Q [R []]. exists R; split; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar