proposition: Lemma osp_distincts : forall A B C P Q, OSP A B C P Q -> A <> B /\ A <> C /\ B <> C /\ A <> P /\ B <> P /\ C <> P /\ A <> Q /\ B <> Q /\ C <> Q.
proof: Proof. intros A B C P Q [R [HPR HQR]]. apply tsp_distincts in HPR. apply tsp_distincts in HQR. spliter; clean; repeat split; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar