proposition: Lemma proj_col : forall A A' C' , A = O -> Col O E A -> Par O E A' C' -> Proj A A' O E' E E' -> A' = O.
proof: Proof. intros. assert(HH:=grid_ok). unfold Proj in H2. spliter. subst A. induction H6. apply False_ind. apply H4. apply par_symmetry. eapply (par_col_par _ _ _ A'); Col. apply par_symmetry. Par. auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg