proposition: Lemma cop__one_or_two_sides : 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. ex_and H X. induction H2; spliter. destruct (or_bet_out C X D) as [|[|]]. left; repeat split; auto; exists X; split; Col. right; apply out_one_side_1 with X; Col. exfalso; Col. induction H; spliter. apply one_or_two_sides_aux with X; assumption. induction (one_or_two_sides_aux A B D C X H1 H0 H H2). left; apply l9_2; assumption. right; apply one_side_symmetry; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar