proposition: Lemma out_one_side_1 : forall A B C D X, ~ Col A B C -> Col A B X -> Out X C D -> OS A B C D.
proof: Proof. intros. induction (eq_dec_points C D). subst D. apply one_side_reflexivity. intro. apply H. Col. prolong C X C' C X. exists C'. assert(TS A B C C'). unfold TS. repeat split. intro. apply H. Col. intro. assert(C'=X). eapply (l6_21 A B C D). assumption. assumption. Col. assumption. apply out_col in H1. eapply (col_transitivity_1 _ X). intro. treat_equalities. Col5. Col. Col. Col. treat_equalities. unfold Out in H1. tauto. exists X. split; Col. assert(TS A B D C'). eapply (l9_5 _ _ _ _ X). apply H5. Col. assumption. split; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar