proposition: Lemma prod_1_l : forall O E E' A, ~ Col O E E' -> Col O E A -> Prod O E E' E A A.
proof: Proof. intros. unfold Prod. repeat split; Col. assert(HH:=(grid_not_par O E E' H)). spliter. 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 H7 B'. unfold unique in H8. spliter. clear H8. unfold Proj in H7. spliter. exists B'. induction H11. repeat split. left; Par. Col. left; Par. subst B'. repeat split; try(apply pj_trivial). Col. Qed.
imports: GeoCoq.Tarski_dev.Ch14_sum