proposition: Lemma one_side_dec : forall A B C D, OS A B C D \/ ~ OS A B C D.
proof: Proof. intros A B C D. destruct (col_dec A B D). right; intro Habs; apply (one_side_not_col124 A B C D); assumption. destruct (l9_10 A B D) as [D']; Col. destruct (two_sides_dec A B C D') as [|HNTS]. left; apply l9_8_1 with D'; assumption. right; intro. apply HNTS, l9_8_2 with D. assumption. apply one_side_symmetry; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar