proposition: Lemma l14_31_1 : forall O E E' A B C D, Ar2_4 O E E' A B C D -> C <> O -> (exists X, Prod O E E' A B X /\ Prod O E E' C D X) -> Prod O C E' A B D.
proof: Proof. intros. ex_and H1 X. spliter. unfold Ar2_4 in H. spliter. induction(eq_dec_points A O). subst A. assert(HH:= prod_0_l O E E' B H H4). assert(X=O). apply (prod_O_l_eq O E E' B); assumption. subst X. apply (prod_null)in H2. induction H2. contradiction. subst D. apply(prod_0_l O C E' B). intro. apply H. ColR. assert(HG:=grid_not_par O E E' H). spliter. ColR. induction(eq_dec_points B O). subst B. assert(HH:= prod_0_r O E E' A H H3). assert(X=O). apply (prod_O_r_eq O E E' A); assumption. subst X. apply (prod_null)in H2. induction H2. contradiction. subst D. apply(prod_0_r O C E' A). intro. apply H. ColR. assert(HG:=grid_not_par O E E' H). spliter. ColR. induction(eq_dec_points D O). subst D. assert(HH:= prod_0_r O E E' C H H5). assert(X=O). apply (prod_O_r_eq O E E' C); assumption. subst X. apply (prod_null)in H1. induction H1. contradiction. contradiction. assert(HG:=grid_not_par O E E' H). spliter. assert(exists ! P' : Tpoint, Proj B P' O E' E' C). apply(project_existence B O E' E' C). intro. subst C. contradiction. auto. intro. induction H16. apply H16. exists E'. split; Col. spliter. apply H. ColR. ex_and H16 B''. unfold unique in H17. spliter. clear H17. unfold Proj in H16. spliter. assert(Par B B'' E' C). induction H20. Par. subst B''. apply False_ind. apply H. ColR. clear H20. unfold Prod. repeat split; try ColR. intro. apply H. ColR. exists B''. split. left. Par. split. Col. assert(HP1:=H1). assert(HP2:=H2). unfold Prod in H1. unfold Prod in H2. spliter. ex_and H22 B'. ex_and H20 D'. assert(B' <> O). intro. subst B'. induction H22. induction H22. apply H22. exists E. split; Col. spliter. apply H. ColR. contradiction. assert(Par E B'' C B'). apply(l13_11 E C B B' B'' E' O); Col. intro. apply H. ColR. ColR. intro. subst B''. induction H21. apply H21. exists C. split; Col. ColR. spliter. apply H. ColR. ColR. Par. induction H22. Par. subst B'. apply False_ind. apply H. ColR. assert(X <> O). intro. subst X. apply prod_null in HP1. induction HP1; contradiction. assert(Par A D' C B'). apply(l13_11 A C X B' D' E' O); Col. intro. apply H. ColR. ColR. unfold Ar2 in *. spliter. ColR. intro. subst D'. induction H20. induction H20. apply H20. exists E. split; Col. spliter. apply H. ColR. contradiction. ColR. induction H26. Par. subst D'. apply False_ind. apply H. unfold Ar2 in *. spliter. ColR. induction H24. Par. subst B'. apply False_ind. unfold Ar2 in *. spliter. apply H. ColR. left. apply par_symmetry. apply par_comm. unfold Ar2 in *. spliter. apply(l13_11 D A E E' B'' D' O); Col. intro. apply H. ColR. ColR. intro. subst B''. induction H28. apply H28. exists C. split; Col. spliter. apply H. ColR. intro. subst D'. induction H30. apply H30. exists C. split; Col. ColR. spliter. apply H. ColR. ColR. apply (par_trans _ _ C B'); Par. induction H20. Par. subst D'. apply False_ind. apply H. ColR. Qed.
imports: GeoCoq.Tarski_dev.Ch14_sum