proposition: Lemma ncop_distincts : forall A B C D, ~ Coplanar A B C D -> A <> B /\ A <> C /\ A <> D /\ B <> C /\ B <> D /\ C <> D.
proof: Proof. intros A B C D H; repeat split; intro; subst; apply H; Cop. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar