proposition: Lemma proj_diff_not_col : forall A B A' B' P Q, A <> A' -> proj A P Q A' -> proj B P Q B' -> (A' <> B' <-> ~Col A B A').
proof: Proof. intros. split. intro. intro. assert(proj B P Q A'). eapply (col_proj_proj A); auto. apply H2. eapply proj_uniqueness. apply H4. assumption. intro. intro. subst B'. apply H2. eapply (proj_eq_col _ _ P Q); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec