proposition: Lemma one_side_col_out : forall A B X Y, Col A X Y -> OS A B X Y -> Out A X Y.
proof: Proof. intros. assert(A <> B /\ ~ Col X A B /\ ~ Col Y A B /\ X <> A /\ Y <> A). unfold OS in H0. ex_and H0 T. unfold TS in *. spliter. repeat split; auto. intro. subst B. Col. intro. subst X. apply H0. Col. intro; spliter. subst Y. apply H1. Col. spliter. induction H. repeat split; auto. induction H. repeat split; auto. right. Between. assert(TS A B X Y). unfold TS. repeat split; auto. exists A. split. Col. Between. apply l9_9 in H6. contradiction. Qed.
imports: GeoCoq.Tarski_dev.Annexes.quadrilaterals_inter_dec