proposition: Lemma pj_uniqueness : forall O E E' A A' A'', ~Col O E E' -> Col O E A -> Col O E' A' -> Col O E' A'' -> Pj E E' A A' -> Pj E E' A A'' -> A' = A''.
proof: Proof. intros. unfold Pj in *. induction(eq_dec_points A O). subst A. assert(HH:= grid_not_par O E E' H). spliter. induction H3. apply False_ind. apply H7. apply par_symmetry. apply (par_col_par _ _ _ A'); Col. subst A'. induction H4. apply False_ind. apply H7. apply par_symmetry. apply (par_col_par _ _ _ A''); Col. auto. induction H3; induction H4. assert(Par A A' A A''). apply (par_trans _ _ E E'); Par. induction H6. apply False_ind. apply H6. exists A. split; Col. spliter. apply(l6_21 O E' A A'); Col. intro. apply H. ColR. auto. subst A''. apply False_ind. apply H. ColR. auto. subst A'. apply False_ind. apply H. ColR. congruence. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg