proposition: Lemma proj_not_col : forall A A' P Q, A <> A' -> proj A P Q A' -> ~Col P Q A.
proof: Proof. intros. unfold proj in H0. spliter. induction H1. spliter. assumption. spliter. subst A'. tauto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec