proposition: Lemma proj_pars : forall A A' C' , A <> O -> Col O E A -> Par O E A' C' -> Proj A A' O E' E E' -> Par_strict O E A' C'.
proof: Proof. intros. unfold Par_strict. assert(HH:=grid_ok). split. apply all_coplanar. intro. ex_and H3 X. unfold Proj in H2. spliter. induction H1. apply H1. exists X. split; Col. spliter. assert(Col A' O E). apply (col_transitivity_1 _ C'); Col. induction(eq_dec_points A' O). subst A'. clean_trivial_hyps. induction H8. induction H7. apply H7. exists E. split; Col. spliter. contradiction. contradiction. apply grid_ok. apply(col_transitivity_1 _ A'); Col. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg