proposition: Lemma col_proj_col : forall A B A' B' P Q, A <> A' -> Col A B A' -> proj A P Q A' -> proj B P Q B' -> Col A B B'.
proof: Proof. intros. induction(eq_dec_points A B). subst B. Col. unfold proj in *. spliter. induction H4; induction H5; spliter. apply col_permutation_2. eapply perp2__col. apply perp_sym. apply H6. apply perp_left_comm. eapply perp_col. assumption. apply perp_sym. apply H8. Col. subst A'. tauto. subst B'. Col. subst B'. Col. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec