proposition: Lemma proj_exists : forall A B T, A <> B -> exists P, proj T A B P.
proof: Proof. intros. induction(col_dec A B T). exists T. unfold proj. split. assumption. right. split; auto. assert(HH:=l8_18_existence A B T H0). ex_and HH P. exists P. unfold proj. split. assumption. left. repeat split;auto. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec