proposition: Lemma cop_dec : forall A B C D, Coplanar A B C D \/ ~ Coplanar A B C D.
proof: Proof. intros A B C D. destruct (col_dec C A B). left; exists C; left; split; Col. destruct (col_dec D A B). left; exists D; left; split; Col. destruct (two_sides_dec A B C D). left; apply ts__coplanar; assumption. destruct (one_side_dec A B C D). left; apply os__coplanar; assumption. right; intro; destruct (cop__one_or_two_sides A B C D); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar