proposition: Lemma prod_exists : forall A B, Col O E A -> Col O E B -> exists C, Prod O E E' A B C.
proof: Proof. intros. assert(NC:=grid_ok). assert(exists! B' : Tpoint, Proj B B' O E' E E'). apply(project_existence B O E' E E'). intro. subst E'. apply NC. Col. intro. subst E'. apply NC. Col. intro. induction H1. apply H1. exists E'. split; Col. spliter. apply NC. Col. ex_and H1 B'. unfold unique in H2. spliter. assert(exists! C, Proj B' C O E E' A). apply(project_existence B' O E E' A). intro. subst E'. apply NC. Col. intro. subst E. apply NC. Col. intro. induction H3. apply H3. exists A. split; Col. spliter. apply NC. Col. ex_and H3 C. unfold unique in H4. spliter. exists C. unfold Prod. repeat split; Col. unfold Proj in H3. tauto. exists B'. repeat split. apply (project_pj B B' O E'). auto. unfold Proj in H1. tauto. apply (project_pj B' C O E). assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch14_sum