proposition: Lemma prod_0_l : forall O E E' A, ~ Col O E E' -> Col O E A -> Prod O E E' O A O.
proof: Proof. intros. unfold Prod. repeat split; Col. assert(HH:=(grid_not_par O E E' H)). spliter. induction(eq_dec_points A O). subst A. exists O. repeat split; try (apply pj_trivial). Col. assert(exists ! P' : Tpoint, Proj A P' O E' E E'). apply(project_existence A O E' E E' H6 H5). intro. apply H3. Par. ex_and H8 B'. unfold unique in H9. spliter. clear H9. unfold Proj in H8. spliter. exists B'. repeat split. induction H12. left. Par. right. assumption. Col. left. right. repeat split; Col. intro. subst B'. induction H12. induction H12. apply H12. exists E. split; Col. spliter. contradiction. contradiction. Qed.
imports: GeoCoq.Tarski_dev.Ch14_sum