proposition: Lemma sum_comm : forall A B C, Sum O E E' A B C -> Sum O E E' B A C.
proof: Proof. intros. induction (eq_dec_points B O). subst B. assert(Col O E A). unfold Sum in H. spliter. unfold Ar2 in H. tauto. assert(C = A). apply (sum_uniqueness A O). auto. apply sum_A_O. auto. subst C. apply sum_O_B. auto. induction(eq_dec_points A O). subst A. assert(Col O E B). unfold Sum in H. spliter. unfold Ar2 in H. tauto. assert(B = C). apply (sum_uniqueness O B). apply sum_O_B. Col. auto. subst C. apply sum_A_O. Col. assert(A <> O \/ B <> O). left. auto. assert(HH:=grid_not_par). spliter. assert(HH := sum_plg A B C H H2). ex_and HH A'. ex_and H9 C'. assert(exists ! P' : Tpoint, Proj B P' O E' E E'). apply(project_existence B O E' E E'); auto. intro. apply H5. Par. unfold unique in H11. ex_and H11 B'. clear H12. assert(HH:= parallel_existence1 O E B' H6). ex_and HH P'. assert(exists! P : Tpoint, Proj A P B' P' O E'). apply(project_existence A B' P' O E'); auto. apply par_distincts in H12. spliter. auto. intro. apply H4. apply(par_trans _ _ B' P'); Par. unfold unique in H13. ex_and H13 D'. clear H14. assert( Ar2 O E E' A B C). unfold Sum in H. tauto. assert(HH:= sum_to_sump O E E' A B C H). unfold Sump in H13. apply sump_to_sum. unfold Sump. unfold Ar2 in H14. spliter. repeat split; Col. exists B'. exists D'. exists P'. split; auto. split; auto. split; auto. assert(Par_strict O E B' P'). induction H12. auto. spliter. apply False_ind. assert(HA:=H11). unfold Proj in H11. spliter. assert(Col B' O E). apply (col_transitivity_1 _ P'); Col. assert(B' <> O). intro. subst B'. apply project_id in HA. contradiction. induction H24. induction H24. apply False_ind. apply H24. exists E. split; Col. spliter. contradiction. contradiction. apply grid_ok. apply (col_transitivity_1 _ B'); Col. assert(Par O A B' D'). apply (par_col_par _ _ _ P'). intro. subst D'. unfold Proj in *. spliter. induction H22. induction H22. apply H22. exists B'. split; Col. spliter. apply grid_ok. apply (col_transitivity_1 _ A); Col. subst B'. apply H18. exists A. split; Col. apply par_symmetry. apply (par_col_par _ _ _ E); Col; Par. unfold Proj in H13. spliter. Col. assert(Par_strict O A B' D'). induction H19. auto. spliter. apply False_ind. apply H18. unfold Proj in H13. spliter. exists O. split. Col. apply col_permutation_2. apply (col_transitivity_1 _ D'); Col. assert(Par O B' A D'). unfold Proj in H13. spliter. induction H24. apply par_symmetry. apply(par_col_par _ _ _ E'); Par. intro. subst B'. apply H20. exists O. split;Col. unfold Proj in H11. spliter. auto. subst D'. apply False_ind. apply H20. exists A. split; Col. assert(Plg O A D' B'). apply(pars_par_plg O A D' B' ); Par. assert(HT:=sum_cong A B C H H2). assert(Parallelogram D' B' B C \/ D' = B' /\ O = A /\ C = B /\ D' = C). apply(plg_pseudo_trans D' B' O A C B). apply plg_to_parallelogram in H22. apply plg_permut in H22. apply plg_permut in H22. auto. right. auto. induction H23. repeat split; auto. apply plg_permut in H23. apply plg_par in H23. unfold Proj in *. spliter. induction H32. left. apply (par_trans _ _ B B'); Par. subst B'. apply par_distincts in H23. tauto. intro. subst B'. apply H20. exists B. split. ColR. Col. intro. subst C. assert(HN:= sum_A_null A B H). contradiction. spliter. subst A. tauto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg