proposition: Lemma proj_eq_col : forall A B P Q C, proj A P Q C -> proj B P Q C -> Col A B C.
proof: Proof. intros. unfold proj in *. spliter. induction H2; induction H1; spliter. apply col_permutation_1. eapply perp2__col. apply perp_sym. apply perp_comm. apply H5. apply perp_sym. Perp. subst B. Col. subst C. Col. subst C. Col. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec