proposition: Lemma proj_diff_not_col_inv : 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. subst B'. eapply (proj_eq_col A B P Q A'); auto. intro. eapply (proj_id A B A' B' P Q); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec