proposition: Lemma tsp__nosp : forall A B C P Q, TSP A B C P Q -> ~ OSP A B C P Q.
proof: Proof. intros A B C P Q HTS HOS. absurd (TSP A B C P P). intro Habs; apply tsp_distincts in Habs; spliter; auto. apply l9_41_2 with Q; [apply l9_38 | apply osp_symmetry]; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar