proposition: Lemma prod_y_axis_change : forall O E E' E'' A B C, Prod O E E' A B C -> ~ Col O E E'' -> Prod O E E'' A B C.
proof: Proof. intros. assert(HP:=H). unfold Prod in H. spliter. unfold Ar2 in H. spliter. assert(HH:=grid_not_par O E E' H ). spliter. ex_and H1 B'. induction(eq_dec_points B O). subst B. assert(Prod O E E' A O O). apply(prod_0_r); Col. assert(HH:= prod_uniqueness O E E' A O C O HP H13). subst C. apply prod_0_r; Col. induction(eq_dec_points A O). subst A. assert(Prod O E E' O B O). apply(prod_0_l); Col. assert(HH:= prod_uniqueness O E E' O B O C H14 HP). subst C. apply(prod_0_l); Col. assert(C <> O). intro. subst C. apply prod_null in HP. induction HP; contradiction. assert(exists ! P' : Tpoint, Proj B P' O E'' E E''). apply(project_existence B O E'' E E''). intro. subst E''. apply H0; Col. intro. subst E''. apply H0; Col. intro. induction H16. apply H16. exists E''. split; Col. spliter. apply H0. Col. ex_and H16 B''. unfold unique in H17. spliter. clear H17. unfold Proj in H16. spliter. assert(Par B B'' E E''). induction H20. Par. subst B''. apply False_ind. apply H0. ColR. clear H20. repeat split; auto. exists B''. repeat split. left; Par. Col. assert(Par E' A B' C). induction H12. assumption. subst B'. apply False_ind. apply H. ColR. clear H12. induction(eq_dec_points B E). subst B. assert(B'' = E''). induction H21. apply False_ind. apply H12. exists E. split; Col. spliter. apply(l6_21 O E'' E E''); Col. subst B''. assert(C = A). assert(Prod O E E' A E A). apply(prod_1_r); Col. eapply (prod_uniqueness O E E' A E); auto. subst C. left. right. repeat split; Col. intro. subst E''. apply H18. right. repeat split; Col. intro. subst E''. apply H18. right. repeat split; Col. assert(Par_strict B B'' E E''). induction H21. assumption. spliter. apply False_ind. apply H0. ColR. assert(Par E E' B B'). induction H1. assumption. subst B'. apply False_ind. apply H. ColR. clear H1. assert(Par_strict E E' B B'). induction H23. assumption. spliter. apply False_ind. apply H. ColR. assert(Par_strict E' A B' C). induction H20. assumption. spliter. apply False_ind. assert(B' <> E'). intro. subst B'. apply H1. exists E'. split; Col. apply H. ColR. induction(eq_dec_points A E). subst A. assert(Prod O E E' E B B). apply prod_1_l; Col. assert(B = C). apply (prod_uniqueness O E E' E B); auto. subst C. left. Par. assert(B' <> O). intro. subst B'. apply H5. apply par_symmetry. apply(par_col_par _ _ _ B); Par. Col. induction(eq_dec_points E' E''). subst E''. assert(Par B B' B B''). apply (par_trans _ _ E E'); Par. induction H27. apply False_ind. apply H27. exists B. split; Col. spliter. assert(B' = B''). apply (l6_21 B B' O E'); Col. intro. apply H. ColR. subst B''. left. Par. induction(col_dec E E' E''). assert(~Col E' E'' A). intro. apply H25. apply (l6_21 O E E' E''); Col. assert(B' <> B''). intro. subst B''. apply H27. assert_diffs. apply(l6_21 O E' B B'); [|ColR..]. intro. apply H. ColR. assert(Par E' E'' B' B''). apply par_comm. apply (par_col_par _ _ _ B); Col. apply par_symmetry. apply (par_col_par _ _ _ E); Col. Par. assert(Par E E' E E''). right. repeat split; Col. assert(Par E E' B B''). apply (par_trans _ _ E E''); Par. assert(Par B B' B B''). apply (par_trans _ _ E E'); Par. induction H33. apply False_ind. apply H33. exists B. split; Col. spliter. Col. assert(B' <> E'). intro. subst B'. apply H1. exists E'. split; Col. assert(Par_strict E' E'' B' B''). induction H31. assumption. spliter. apply False_ind. apply H31. apply(l6_21 O E' E E');Col. ColR. left. apply(l13_15 E' E'' A B' B'' C O H29); Col. apply all_coplanar. ColR. assert(Par E'' E' B'' B'). apply(l13_15 E E'' E' B B'' B' O ); Par. Col. apply all_coplanar. induction(col_dec A E' E''). assert(Par B' C E' E''). apply (par_col_par _ _ _ A); Par. Col. assert(Par B' C B' B''). apply (par_trans _ _ E' E''); Par. induction H32. apply False_ind. apply H32. exists B'. split; Col. spliter. left. apply par_comm. apply(par_col_par _ _ _ B'); Par. intro. subst B''. apply H22. exists E. split; ColR. apply par_symmetry. apply(par_col_par _ _ _ E'); Par. intro. subst E''. apply H22. exists B. split; ColR. assert(B' <> E'). intro. subst B'. apply H24. exists E'. split; Col. assert(B'' <> E''). intro. subst B''. apply H22. exists E''. split; Col. induction H29. left. apply(l13_15 E' E'' A B' B'' C O ); Par. intro. apply H30. Col. apply all_coplanar. ColR. spliter. induction(col_dec O E' E''). left. apply par_comm. apply (l13_19 E E' A E'' B B' C B'' O); Col. intro. subst B''. apply H22. exists E. split; Col. ColR. left. Par. apply False_ind. apply H31. apply (l6_21 O E' E'' E'); Col. ColR. Qed.
imports: GeoCoq.Tarski_dev.Ch14_sum