proposition: Lemma prod_x_axis_unit_change : forall O E E' A B C D U, Ar2_4 O E E' A B C D -> Col O E U -> U <> O -> ( exists X, Prod O E E' A B X /\ Prod O E E' C D X) -> ( exists Y, Prod O U E' A B Y /\ Prod O U E' C D Y).
proof: Proof. intros. ex_and H2 X. 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(X = O). apply(prod_O_l_eq O E E' B); assumption. subst X. apply prod_null in H3. induction H3. subst C. exists O. split. apply(prod_0_l). intro. apply H. ColR. ColR. apply(prod_0_l). intro. apply H. ColR. ColR. subst D. exists O. split. apply(prod_0_l). intro. apply H. ColR. ColR. apply(prod_0_r). intro. apply H. ColR. ColR. induction(eq_dec_points B O). subst B. assert(X = O). apply(prod_O_r_eq O E E' A); assumption. subst X. apply prod_null in H3. induction H3. subst C. exists O. split. apply(prod_0_r). intro. apply H. ColR. ColR. apply(prod_0_l). intro. apply H. ColR. ColR. subst D. exists O. split. apply(prod_0_r). intro. apply H. ColR. ColR. apply(prod_0_r). intro. apply H. ColR. ColR. induction(eq_dec_points C O). subst C. assert(X = O). apply(prod_O_l_eq O E E' D); assumption. subst X. apply prod_null in H2. induction H2. subst A. exists O. split. apply(prod_0_l). intro. apply H. ColR. ColR. apply(prod_0_l). intro. apply H. ColR. ColR. subst B. exists O. split. apply(prod_0_r). intro. apply H. ColR. ColR. apply(prod_0_l). intro. apply H. ColR. ColR. induction(eq_dec_points D O). subst D. assert(X = O). apply(prod_O_r_eq O E E' C); assumption. subst X. apply prod_null in H2. induction H2. subst A. exists O. split. apply(prod_0_l). intro. apply H. ColR. ColR. apply(prod_0_r). intro. apply H. ColR. ColR. subst B. exists O. split. apply(prod_0_r). intro. apply H. ColR. ColR. apply(prod_0_r). intro. apply H. ColR. ColR. assert(exists ! P' : Tpoint, Proj B P' O E' U E'). apply(project_existence B O E' U E'). intro. subst U. contradiction. auto. intro. induction H18. apply H18. exists E'. split;Col. spliter. apply H. ColR. ex_and H18 Bu. unfold unique in H19. spliter. clear H19. unfold Proj in H18. spliter. assert(Par B Bu U E'). induction H22. Par. subst Bu. apply False_ind. apply H. ColR. clear H22. assert(exists ! P' : Tpoint, Proj Bu P' O E A E'). apply(project_existence Bu O E A E'). intro. subst A. contradiction. auto. intro. induction H22. apply H22. exists A. split; Col. spliter. apply H. Col. ex_and H22 Xu. unfold unique in H24. spliter. clear H24. unfold Proj in H22. spliter. assert(Par Bu Xu A E'). induction H27. Par. subst Bu. apply False_ind. induction H23. apply H23. exists U. split; Col. ColR. spliter. apply H. ColR. clear H27. exists Xu. split. unfold Prod. repeat split; try ColR. intro. apply H. ColR. exists Bu. split. left. Par. split. ColR. left. Par. assert(exists ! P' : Tpoint, Proj D P' O E' U E'). apply(project_existence D O E' U E'). intro. subst U. apply H. ColR. auto. intro. induction H27. apply H27. exists E'. split; Col. spliter. apply H. ColR. ex_and H27 Du. unfold unique in H29. spliter. clear H29. unfold Proj in H27. spliter. assert(Par D Du U E'). induction H32. Par. subst Du. apply False_ind. apply H. ColR. clear H32. unfold Prod. repeat split; try ColR. intro. apply H. ColR. exists Du. split. left. Par. split. Col. assert(Prod O C E' A B D). apply(l14_31_1 O E E' A B C D). repeat split; Col. auto. exists X. split; Col. unfold Prod in H2. spliter. ex_and H34 B'. unfold Prod in H3. spliter. ex_and H37 D'. unfold Prod in H32. spliter. ex_and H40 D''. assert(Xu <> O). intro. subst Xu. induction H28. apply H28. exists E'. split; Col. spliter. apply H. ColR. assert(D'' <> O). intro. subst D''. induction H42. induction H42. apply H42. exists A. split; Col. ColR. spliter. apply H. ColR. subst D. tauto. assert(Par Xu Du B D''). apply(l13_11 Xu B D D'' Du Bu O); auto. intro. apply H. ColR. ColR. ColR. intro. subst Du. induction H33. apply H33. exists U. split; Col. ColR. spliter. apply H. ColR. intro. subst Bu. induction H28. apply H28. exists A. split; Col. ColR. spliter. apply H. ColR. ColR. ColR. apply(par_trans _ _ U E'); Par. induction H42. apply (par_trans _ _ E' A); Par. subst D''. apply False_ind. apply H. ColR. left. apply (par_trans _ _ B D''); Par. induction H40. Par. subst D''. apply False_ind. apply par_distincts in H45. tauto. Qed.
imports: GeoCoq.Tarski_dev.Ch14_sum