proposition: Lemma proj_not_eq : forall A B A' B' P Q, A' <> B' -> proj A P Q A' -> proj B P Q B' -> A <> B.
proof: Proof. intros. intro. apply H. eapply proj_uniqueness. apply H0. subst B. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec