proposition: Lemma cop_nts__os : forall A B C D, Coplanar A B C D -> ~ Col C A B -> ~ Col D A B -> ~ TS A B C D -> OS A B C D.
proof: Proof. intros. induction (cop__one_or_two_sides A B C D); auto. contradiction. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar