proposition: Lemma proj_inv_exists : forall P Q A', P <> Q -> Col P Q A' -> exists A, A <> A' /\ proj A P Q A'.
proof: Proof. intros. assert(HH0:= not_col_exists P Q H). ex_and HH0 X. induction(eq_dec_points A' P). subst P. assert(Q <> A'). intro. apply H. auto. apply col_permutation_1 in H0. assert(~Col Q A' X). intro. apply H1. Col. assert(HH:= ex_per_cong Q A' A' X A' Q H2 H H0 H3). ex_and HH A. exists A. split. intro. subst A'. apply cong_symmetry in H5. apply cong_identity in H5. contradiction. eapply per_proj; auto. apply l8_5. Col. assert(HH:= ex_per_cong P Q A' X P Q H H H0 H1). ex_and HH A. exists A. split. intro. subst A'. apply cong_symmetry in H4. apply cong_identity in H4. contradiction. apply per_proj; auto. apply per_col with P. auto. assumption. Col. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec