proposition: Lemma os_distincts : forall A B X Y, OS A B X Y -> A <> B /\ A <> X /\ A <> Y /\ B <> X /\ B <> Y.
proof: Proof. intros A B P Q HOS. destruct HOS as [Z [HTS1 HTS2]]. apply ts_distincts in HTS1. apply ts_distincts in HTS2. spliter. repeat split; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar