proposition: Lemma sum_x_axis_unit_change : forall O E E' U A B C, Sum O E E' A B C -> Col O E U -> U <> O -> Sum O U E' A B C.
proof: Proof. intros. induction (eq_dec_points U E). subst U. assumption. assert(HS:= H). assert(Ar2 O E E' A B C). unfold Sum in H. tauto. assert(HA:=H3). unfold Ar2 in H3. spliter. assert(HH:=grid_not_par O E E' H3). spliter. assert(~Col O U E'). intro. apply H3. ColR. assert(HH:=grid_not_par O U E' H13). spliter. induction(eq_dec_points A O). subst A. apply sum_O_B_eq in H; Col. subst C. apply sum_O_B; Col. ColR. induction(eq_dec_points B O). subst B. apply sum_A_O_eq in H; Col. subst C. apply sum_A_O; Col. ColR. apply sum_plg in H; auto. ex_and H A'. ex_and H22 C'. apply plg_to_parallelogram in H. apply plg_to_parallelogram in H22. assert(Ar2 O U E' A B C). repeat split ; auto; ColR. assert(HB:= H23). unfold Ar2 in H23. spliter. clean_duplicated_hyps. assert(exists ! P' : Tpoint, Proj A P' O E' U E'). apply(project_existence A O E' U E' H19 H11 ). intro. apply H16. Par. ex_and H18 A''. unfold unique in H23. spliter. clear H23. unfold Proj in H18. spliter. clean_duplicated_hyps. assert(Par A A'' U E'). induction H29. assumption. subst A''. apply False_ind. apply H3. ColR. clear H29. assert(HH:= plg_existence B O A'' H21). ex_and HH C''. assert(O <> A''). intro. subst A''. assert(HH:=plg_trivial B O H21). assert(B = C''). apply (plg_uniqueness B O O B C''); auto. subst C''. induction H18. apply H18. exists U. split; Col. spliter. apply H3. ColR. assert(HP1:=H23). apply plg_par in H23; auto. spliter. repeat split; auto. exists A''. exists C''. repeat split. left. Par. Col. left. assert(Par O U B O). right. repeat split; Col. apply (par_trans _ _ B O); Par. left. assert(Par O E' O A''). right. repeat split; Col. apply(par_trans _ _ O A''); Par. assert(Parallelogram_flat O A C B). apply(sum_cong O E E' H3 A B C HS); auto. assert(Parallelogram O A C B). right. assumption. assert(Parallelogram A C C'' A'' \/ A = C /\ B = O /\ A'' = C'' /\ A = A''). apply(plg_pseudo_trans A C B O A'' C''). apply plg_permut. assumption. assumption. assert(Parallelogram A C C'' A''). induction H32. assumption. spliter. contradiction. clear H32. apply plg_par in H33. left. spliter. apply(par_trans _ _ A A''); Par. intro. subst C. apply sum_B_null in HS. contradiction. auto. intro. subst C''. induction H23. apply H23. exists C. split; Col. ColR. spliter. apply H3. ColR. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg