proposition: Lemma change_grid_prod : forall O E E' A B C O' A' B' C', Par_strict O E O' E' -> Ar1 O E A B C -> Ar1 O' E' A' B' C' -> Pj O O' E E' -> Pj O O' A A' -> Pj O O' B B' -> Pj O O' C C' -> Prod O E E' A B C -> Prod O' E' E A' B' C'.
proof: Proof. intros. induction (eq_dec_points A O). subst A. apply(change_grid_prod_l_O O E E' B C O' A' B' C'); auto. induction (eq_dec_points B O). subst B. apply prod_comm. unfold Ar1 in *. spliter. apply(change_grid_prod_l_O O E E' A C O' B' A' C'); auto. repeat split; Col. repeat split; Col. apply prod_comm. assumption. induction(eq_dec_points C O). subst C. apply prod_null in H6. induction H6;contradiction. induction(eq_dec_points A E). subst A. apply (change_grid_prod1 O E E' B C); auto. rename H10 into ANE. assert(HP:=H6). unfold Prod in H6. spliter. clear H10. unfold Ar1 in *. unfold Ar2 in H6. spliter. clean_duplicated_hyps. prolong O O' E'' O O'. assert(E''<> O). intro. subst E''. apply between_identity in H10. subst O'. apply H. exists O. split; Col. assert(~Col O E E''). intro. apply H. exists O'. apply bet_col in H10. split; Col. ColR. assert(HH:= prod_y_axis_change O E E' E'' A B C HP H19). assert(HP1:= HH). unfold Prod in HH. spliter. ex_and H21 B''. assert(~Col O E'' E). intro. apply H19. Col. assert(exists C : Tpoint, Sum O E'' E E'' O' C). apply(sum_exists O E'' E H24 E'' O'); Col. ex_and H25 C2. assert(~ Col O E'' A). intro. apply H24. ColR. assert(HH:= sum_y_axis_change O E'' E A E'' O' C2 H26 H25). assert(HS1:= HH). unfold Sum in HH. spliter. unfold Ar2 in H27. spliter. clear H27. ex_and H28 A0. ex_and H27 A0'. assert(A = A0). apply(l6_21 O E E'' A); Col. intro. subst A. apply H25. Col. ColR. induction H27. induction H27. apply False_ind. apply H27. exists E''. split; Col. spliter. Col. subst A0. Col. subst A0. assert(Par O O' E E'). induction H2. Par. subst E'. apply False_ind. apply H6. Col. assert(Par O O' A A'). induction H3. Par. subst A'. apply False_ind. apply H. exists A. split; Col. assert(Par O O' B B'). induction H4. Par. subst B'. apply False_ind. apply H. exists B. split; Col. assert(Par O O' C C'). induction H5. Par. subst C'. apply False_ind. apply H. exists C. split; Col. assert(O <> O'). intro. subst O'. apply par_distinct in H35. tauto. clear H2 H3 H4 H5. assert(A0'=A'). apply (l6_21 O' E' A A'); Col. intro. apply H. exists A. split; Col. intro. subst A'. apply par_distinct in H36. tauto. induction H33. assert(Par O' E' O' A0'). apply(par_trans _ _ O A); Par. apply(par_col_par _ _ _ E); Col. left. Par. induction H3. apply False_ind. apply H3. exists O'. split; Col. spliter. Col. subst A0'. Col. induction H32. assert(Par A A' A A0'). apply(par_trans _ _ O O'); Par. apply par_symmetry. apply(par_col_par _ _ _ E''); Col. Par. induction H3. apply False_ind. apply H3. exists A. split; Col. spliter. Col. subst A0'. Col. subst A0'. assert(Par O E'' A A'). induction H32. Par. subst A'. apply par_distinct in H36. tauto. assert(Par O A O' A'). induction H33. Par. subst A'. apply False_ind. induction H2. apply H2. exists O'. split; Col. spliter. apply H. exists O'. split; Col. ColR. assert(Par A E'' A' C2). induction H34. Par. subst C2. apply False_ind. induction H2. apply H2. exists A'. split; Col. spliter. apply H. exists A'. split; Col. ColR. clear H33 H34 H32. assert(HS0:= H26). induction H26. unfold Ar2 in H5. spliter. clean_duplicated_hyps. ex_and H26 E0. ex_and H5 E0'. assert(E0 = E). apply (l6_21 E'' E O E); Col. induction H5. induction H5. apply False_ind. apply H5. exists E''. split; Col. spliter. Col. subst E0. Col. subst E0. assert(E0' = E'). apply(l6_21 O' E' E E'); Col. intro. apply H. exists E. split; Col. intro. subst E'. apply H6. Col. induction H30. assert(Par O' E' O' E0'). apply(par_trans _ _ O E); Par. induction H40. apply False_ind. apply H40. exists O'. split; Col. spliter. Col. subst E0'. Col. induction H29. assert(Par E E' E E0'). apply(par_trans _ _ O E''); Par. apply (par_col_par _ _ _ O'); Col. Par. induction H40. apply False_ind. apply H40. exists E. split; Col. spliter. Col. subst E0'. Col. subst E0'. clean_trivial_hyps. clean_duplicated_hyps. assert(Par E E'' E' C2). induction H31. Par. subst C2. apply False_ind. assert(Col O O' E'). ColR. apply H. exists O. split; Col. clear H31. clear H5. clear H30. clear H29. assert(Par E E'' B B''). induction H21. Par. subst B''. apply False_ind. apply H19. ColR. clear H21. assert(exists C : Tpoint, Sum O E'' E B'' O' C). apply(sum_exists O E'' E H24 B'' O'); Col. ex_and H21 C3. assert(HS2:= H28). induction H28. ex_and H28 B0. ex_and H29 B0'. assert(B'' <> O). intro. subst B''. induction H5. apply H5. exists E. split; Col. spliter. apply H19. ColR. assert(B0 = B). apply (l6_21 O E B'' B); Col. intro. apply H24. ColR. intro. subst B''. apply par_distinct in H5. tauto. induction H28. assert(Par B'' B0 B B''). apply(par_trans _ _ E E''); Par. induction H41. apply False_ind. apply H41. exists B''. split; Col. spliter. Col. subst B0. Col. subst B0. assert(B0' = B'). apply (l6_21 O' E' B B'); Col. intro. apply H. exists B. split; Col. intro. subst B'. apply par_distinct in H37. tauto. induction H31. assert(Par O' E' O' B0'). apply(par_trans _ _ O E); Par. induction H41. apply False_ind. apply H41. exists O'. split; Col. spliter. Col. subst B0'. Col. induction H30. assert(Par B B' B B0'). apply(par_trans _ _ O E''); Par. apply (par_col_par _ _ _ O'); Col. Par. induction H41. apply False_ind. apply H41. exists B. split; Col. spliter. Col. subst B0'. Col. subst B0'. unfold Ar2 in H21. spliter. clean_duplicated_hyps. assert(E'' <> O). intro. subst E''. apply H25. Col. assert(B' <> O'). intro. subst B'. induction H37. apply H29. exists O'. split; Col. spliter. apply H. exists O'. split; Col. ColR. assert(Par E E'' B' C3). induction H32. Par. subst C3. apply False_ind. assert(Col O O' B'). ColR. apply H. exists O. split; Col. ColR. clear H32. assert(Par E'' E B'' B). induction H28. Par. subst B''. apply par_distinct in H5. tauto. clear H28. assert(HH:= sum_y_axis_change O E'' E A B'' O' C3 HS2 H25). assert(HS3 := HH). unfold Sum in HH. spliter. unfold Ar2 in H28. spliter. clean_duplicated_hyps. ex_and H42 C0. ex_and H21 C0'. assert(Par E'' A B'' C). induction H23. Par. subst B''. apply False_ind. induction H32. apply H23. exists E. split; Col. ColR. spliter. apply H19. ColR. clear H23. assert(C0 = C). apply (l6_21 O E B'' C); Col. intro. apply H19. ColR. intro. subst B''. apply par_distinct in H46. tauto. ColR. induction H21. assert(Par B'' C B'' C0). apply(par_trans _ _ E'' A); Par. induction H23. apply False_ind. apply H23. exists B''. split; Col. spliter. Col. subst C0. Col. subst C0. assert(C0' = C'). apply (l6_21 O' E' C C'); Col. intro. apply H. exists C. split; Col. intro. subst C'. apply par_distincts in H38. tauto. induction H44. assert(Par O' C' O' C0'). apply(par_trans _ _ O E); Par. apply par_symmetry. apply(par_col_par _ _ _ E'); Col. intro. subst C'. induction H38. apply H38. exists O'. split; Col. spliter. apply H. exists O'. split; Col. ColR. left. Par. apply par_symmetry. apply(par_col_par _ _ _ A); Col. Par. induction H44. apply False_ind. apply H44. exists O'. split; Col. spliter. Col. ColR. subst C0'. Col. induction H42. assert(Par C C' C C0'). apply(par_trans _ _ O O'); Par. apply par_symmetry. apply (par_col_par _ _ _ E''); Col. Par. induction H42. apply False_ind. apply H42. exists C. split; Col. spliter. Col. subst C0'. induction H44. induction H23. apply False_ind. apply H23. exists C. split;Col. spliter. apply False_ind. apply H. exists O'. split; Col. ColR. Col. subst C0'. assert(Par B B'' B' C3). apply(par_trans _ _ E E''); Par. assert(Par C B'' C' C3). apply(par_trans _ _ A E''); Par. induction H45. Par. subst C3. assert(Par E E'' O E). apply(par_trans _ _ O' E'); Par. apply(par_col_par _ _ _ C'); Col. apply par_comm. apply(par_col_par _ _ _ B'); Col. intro. subst C'. induction H38. apply H38. exists O'. split; Col. spliter. apply H. exists O'. split; Col. ColR. Par. ColR. apply False_ind. induction H45. apply H45. exists E. split; Col. spliter. apply H24. Col. assert(Prod O' E' C2 A' B' C'). repeat split; Col. intro. assert(C2 <> O'). intro. subst C2. assert(Par O E E E''). apply(par_trans _ _ O' E'); Par. induction H49. apply H49. exists E. split; Col. spliter. contradiction. assert(Col O O' C2). ColR. assert(Col O O' E'). ColR. apply H. exists O. split; Col. exists C3. split. left. apply (par_trans _ _ B B''); Par. apply (par_trans _ _ E E''); Par. split. ColR. left. apply(par_trans _ _ C B''); Par. apply(par_trans _ _ A E''); Par. apply(prod_y_axis_change O' E' C2 E A' B' C' H48). intro. apply H. exists E. split; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch14_sum