proposition: Lemma proj_one_side : forall A B A' B' P Q, A <> A' -> proj A P Q A' -> proj B P Q B' -> Col B A A' \/ OS A A' B B'.
proof: Proof. intros. induction (col_dec B A A'). left. assumption. induction(eq_dec_points B B'). subst B'. right. apply one_side_reflexivity. assumption. assert(Par A A' B B'). unfold proj in *. spliter. induction H5; induction H4;spliter. eapply l12_9_2D. apply perp_sym. apply H8. Perp. subst B'. tauto. subst A'. tauto. subst B'. tauto. assert(Par_strict A A' B B'). induction H4. assumption. spliter. apply False_ind. apply H2. ColR. right. eapply l12_6. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec