proposition: Lemma proj_not_eq_not_col : forall A B A' B' P Q, A' <> B' -> A <> A' -> proj A P Q A' -> proj B P Q B' -> ~Col A A' B'.
proof: Proof. intros. unfold proj in H1. spliter. induction H3; spliter. assert(Col P Q B'). apply col_permutation_1. eapply proj_col. apply H2. induction(eq_dec_points P A'). subst P. assert(Perp A' B' A A'). apply perp_col with Q. auto. apply perp_left_comm. apply perp_col with A'. auto. apply perp_left_comm. apply H4. Col. Col. assert(~Col A' A B'). eapply perp_not_col. apply perp_comm. Perp. intro. apply H8. Col. assert(Perp A' B' A A'). apply perp_col with P. assumption. apply perp_left_comm. apply perp_col with Q. auto. assumption. assumption. ColR. assert(~Col A' A B'). eapply perp_not_col. apply perp_comm. Perp. intro. apply H9. Col. subst A'. tauto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec