proposition: Lemma sum_y_axis_change : forall O E E' E'' A B C, Sum O E E' A B C -> ~ Col O E E'' -> Sum O E E'' A B C.
proof: Proof. intros. assert(HS:= H). assert(Ar2 O E E' A B C). unfold Sum in H. tauto. assert(HA:=H1). unfold Ar2 in H1. spliter. assert(HH:=grid_not_par O E E' H1). spliter. induction(eq_dec_points A O). subst A. apply sum_O_B_eq in H; Col. subst C. apply sum_O_B; Col. induction(eq_dec_points B O). subst B. apply sum_A_O_eq in H; Col. subst C. apply sum_A_O; Col. apply sum_plg in H; auto. ex_and H A'. ex_and H13 C'. assert(exists ! P' : Tpoint, Proj A P' O E'' E E''). apply(project_existence A O E'' E E''); intro; try (subst E''; apply H0; Col). induction H14. apply H14. exists E''. split; Col. spliter. apply H0. Col. ex_and H14 A''. unfold unique in H15. spliter. clear H15. unfold Proj in H14. spliter. assert(Par A A'' E E''). induction H18; auto. subst A''. apply False_ind. apply H0. ColR. clear H18. assert(HH:= plg_existence B O A'' H12). ex_and HH C''. apply plg_to_parallelogram in H. apply plg_to_parallelogram in H13. assert(A'' <> O). intro. subst A''. induction H19. apply H19. exists E. split; Col. spliter. contradiction. repeat split; Col. exists A''. exists C''. repeat split. left. Par. Col. apply plg_par in H18; auto. spliter. left. apply par_symmetry. apply (par_col_par _ _ _ B); Par; Col. apply plg_par in H18; auto. spliter. left. apply par_symmetry. apply (par_col_par _ _ _ A''); Par; Col. left. assert(Parallelogram_flat O A C B). apply(sum_cong O E E' H1 A B C HS). left; auto. assert(Parallelogram O A C B). right; auto. assert(Parallelogram C'' A'' A C \/ C'' = A'' /\ O = B /\ C = A /\ C'' = C). apply(plg_pseudo_trans C'' A'' O B C A). apply plg_comm2. apply plg_permut. apply plg_permut. assumption. apply plg_permut in H22. apply plg_comm2. apply plg_permut. apply plg_permut. assumption. assert(Parallelogram C'' A'' A C). induction H23. assumption. spliter. subst B. tauto. clear H23. assert(A <> C). intro. subst C. assert(Parallelogram O A A O). apply(plg_trivial O A); auto. assert(HH:=plg_uniqueness O A A O B H23 H22). subst B. tauto. assert(A <> A''). intro. subst A''. apply par_distincts in H19. tauto. assert(A'' <> C''). intro. subst C''. assert(Parallelogram A'' A'' A A). apply(plg_trivial1); auto. assert(HH:= plg_uniqueness A'' A'' A A C H26 H24). contradiction. apply plg_par in H24; auto. spliter. apply(par_trans _ _ A'' A); Par. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg