proposition: Lemma l14_31_2 : forall O E E' A B C D , Ar2_4 O E E' A B C D -> C <> O -> Prod O C E' A B D -> (exists X, Prod O E E' A B X /\ Prod O E E' C D X).
proof: Proof. intros. unfold Ar2_4 in H. spliter. assert(HG:= grid_not_par O E E' H). spliter. induction(eq_dec_points A O). subst A. assert(D = O). apply(prod_O_l_eq O C E' B); auto. subst D. exists O. split. apply(prod_0_l O E E' B); Col. apply(prod_0_r O E E' C); Col. induction(eq_dec_points B O). subst B. assert(D = O). apply(prod_O_r_eq O C E' A); auto. subst D. exists O. split. apply(prod_0_r O E E' A); Col. apply(prod_0_r O E E' C); Col. induction(eq_dec_points D O). subst D. exists O. apply prod_null in H1. induction H1. subst A. split. apply(prod_0_l O E E' B); Col. apply(prod_0_r O E E' C); Col. subst B. split. apply(prod_0_r O E E' A); Col. apply(prod_0_r O E E' C); Col. assert(exists ! P' : Tpoint, Proj B P' O E' E E'). apply(project_existence B O E' E E'); auto. intro. apply H8. Par. ex_and H15 B'. unfold unique in H16. spliter. clear H16. unfold Proj in H15. spliter. assert(Par B B' E E'). induction H19. Par. subst B'. apply False_ind. apply H. ColR. clear H19. assert(exists ! P' : Tpoint, Proj B' P' O E E' A). apply(project_existence B' O E E' A); auto. intro. subst A. contradiction. intro. induction H19. apply H19. exists A. split; Col. spliter. apply H. Col. ex_and H19 X. unfold unique in H21. spliter. clear H21. unfold Proj in H19. spliter. clean_duplicated_hyps. assert(X <> O). intro. subst X. induction H24. induction H15. apply H15. exists E'. split; Col. spliter. apply H. ColR. subst B'. induction H20. apply H15. exists E. split; Col. spliter. contradiction. assert(Par B' X E' A). induction H24. Par. subst B'. apply False_ind. apply H. ColR. clear H24. exists X. unfold Prod in *. spliter. ex_and H17 B''. repeat split; Col. exists B'. split. left. Par. split. Col. induction H24. left. Par. subst B''. apply False_ind. apply H. ColR. assert(exists ! P' : Tpoint, Proj D P' O E' E E'). apply(project_existence D O E' E E'); Col. intro. apply H8. Par. ex_and H25 D'. unfold unique in H26. spliter. clear H26. unfold Proj in H25. spliter. clean_duplicated_hyps. assert(Par D D' E E'). induction H29. Par. subst D'. apply False_ind. apply H. ColR. clear H29. exists D'. split. left. Par. split. Col. left. assert(Par X D' B B''). apply(l13_11 X B D B'' D' B' O); auto. intro. assert(B''<>O). intro. subst B''. induction H17. induction H17. apply H17. exists C. split; Col. ColR. spliter. apply H. ColR. contradiction. apply H. ColR. ColR. ColR. intro. subst D'. induction H25. apply H25. exists E. split; Col. spliter. contradiction. intro. subst B'. induction H20. apply H20. exists E. split; Col. spliter. contradiction. ColR. ColR. Par. apply(par_trans _ _ E E'); Par. induction H24. apply(par_trans _ _ E' A); Par. subst B''. apply False_ind. apply H. ColR. induction H17. apply (par_trans _ _ B B''); Par. subst B''. apply par_distincts in H26. tauto. Qed.
imports: GeoCoq.Tarski_dev.Ch14_sum