proposition: Lemma os__coplanar : forall A B C D, OS A B C D -> Coplanar A B C D.
proof: Proof. intros A B C D HOS. assert (HNCol : ~ Col A B C) by (apply one_side_not_col123 with D, HOS). destruct (segment_construction C B B C) as [C'[]]. assert (HT : TS A B D C'). { apply l9_8_2 with C; [|assumption]. split; [|split]. Col. intro; apply HNCol; ColR. exists B; split; Col. } destruct HT as [HNCol1 [HNCol2 [T []]]]. assert (C' <> T) by (intro; treat_equalities; auto). destruct (col_dec T B C) as [|HNCol3]. exists B; left; split; ColR. destruct (bet_dec T B A) as [|HOut]. - apply coplanar_perm_18, ts__coplanar. apply l9_8_2 with T. repeat split; Col; exists B; split; Col. apply out_one_side_1 with C'; Col. apply bet_out; Between. - apply coplanar_perm_19, ts__coplanar, l9_31; [|apply one_side_symmetry, invert_one_side, HOS]. apply one_side_transitivity with T. apply out_one_side_1 with C'; [intro; apply HNCol3; ColR|Col|apply l6_6, bet_out; Between]. apply out_one_side; Col; apply not_bet_out; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar