proposition: Lemma osp__ncop1 : forall A B C P Q, OSP A B C P Q -> ~ Coplanar A B C P.
proof: Proof. intros A B C P Q [R [H1 H2]]. apply tsp__ncop1 with R, H1. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar