proposition: Lemma ncop__ncols : forall A B C D, ~ Coplanar A B C D -> ~ Col A B C /\ ~ Col A B D /\ ~ Col A C D /\ ~ Col B C D.
proof: Proof. intros; repeat split. apply ncop__ncol with D, H. apply ncop__ncol with C, ncoplanar_perm_1, H. apply ncop__ncol with B, ncoplanar_perm_3, H. apply ncop__ncol with A, ncoplanar_perm_9, H. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality