proposition: Lemma Pj_exists : forall A B C, exists D, Pj A B C D.
proof: Proof. intros. unfold Pj in *. elim (eq_dec_points A B);intro. subst. exists C. tauto. assert (T:=parallel_existence A B C H). decompose [and ex] T;clear T. exists x0. induction (eq_dec_points C x0). tauto. eauto using par_col2_par with col. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg