proposition: Lemma osp_reflexivity : forall A B C P, ~ Coplanar A B C P -> OSP A B C P P.
proof: Proof. intros A B C P HP. destruct (tsp_exists A B C P HP) as [Q]. exists Q; split; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar