proposition: Lemma osp__ntsp : forall A B C P Q, OSP A B C P Q -> ~ TSP A B C P Q.
proof: Proof. intros A B C P Q HOS HTS. apply (tsp__nosp A B C P Q); assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar