proposition: Lemma col_one_side_out : forall A B X Y, Col A X Y -> OS A B X Y -> Out A X Y.
proof: Proof. intros. assert(X <> A /\ Y <> A). unfold OS in H0. ex_and H0 Z. unfold TS in *. spliter. ex_and H5 T0. ex_and H3 T1. split. intro. subst X. Col. intro. subst Y. Col. spliter. unfold Col in H. induction H. unfold Out. repeat split; try assumption. left. assumption. induction H. unfold Out. repeat split; try assumption. right. apply between_symmetry. assumption. assert(TS A B X Y). unfold TS. assert(HH0 := H0). unfold OS in H0. ex_and H0 Z. unfold TS in *. spliter. repeat split. assumption. assumption. exists A. split. apply col_trivial_1. apply between_symmetry. assumption. eapply l9_9 in H3. contradiction. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar