proposition: Lemma change_grid_sum : 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' -> Sum O E E' A B C -> Sum O' E' E A' B' C'.
proof: Proof. intros. induction(eq_dec_points A O). subst A. apply(change_grid_sum_0 O E E' O B C); auto. assert(HS:= H6). induction H6. ex_and H8 A1. ex_and H9 C1. unfold Ar1 in *. unfold Ar2 in H6. spliter. assert(HG:=grid_not_par O E E' H6). spliter. assert(~Col O' E' E). intro. apply H. exists E. split; Col. assert(HG:=grid_not_par O' E' E H28). spliter. clean_duplicated_hyps. induction(eq_dec_points B O). subst B. apply sum_comm; Col. apply sum_comm in HS; Col. apply(change_grid_sum_0 O E E' O A C); auto. repeat split; auto. repeat split; auto. assert(A' <> O). intro. subst A'. induction H3. induction H3. apply H3. exists O. split; Col. spliter. apply H. exists O'. split; Col. ColR. contradiction. assert(~Col O A A'). intro. apply H. exists A'. split; Col. ColR. assert(A' <> O'). intro. subst A'. induction H3. induction H3. apply H3. exists O'. split; Col. spliter. contradiction. subst A. apply H15. Col. assert(Parallelogram_flat O A C B). apply(sum_cong O E E' H6 A B C HS). left. auto. unfold Parallelogram_flat in H32. spliter. assert(Proj O O' O' E' E E'). unfold Proj. repeat split; Col. intro. apply H29. Par. induction H2. left; Par. subst E'. tauto. assert(Proj A A' O' E' E E'). unfold Proj. repeat split; Col. intro. apply H29. Par. induction H3. left. induction H2. apply (par_trans _ _ O O'); Par. subst E'. tauto. subst A'. right. auto. assert(Proj C C' O' E' E E'). unfold Proj. repeat split; Col. intro. apply H29. Par. induction H5. left. induction H2. apply (par_trans _ _ O O'); Par. subst E'. tauto. right. auto. assert(Proj B B' O' E' E E'). unfold Proj. repeat split; Col. intro. apply H29. Par. induction H4. left. induction H2. apply (par_trans _ _ O O'); Par. subst E'. tauto. right. auto. assert(EqV O A B C). unfold EqV. left. right. apply plgf_permut. unfold Parallelogram_flat. repeat split; Col; Cong. ColR. induction H38. right. auto. left. auto. assert(HH:=project_preserves_eqv O A B C O' A' B' C' O' E' E E' H43 H39 H40 H42 H41). unfold EqV in HH. induction HH. assert(Parallelogram_flat O' A' C' B'). induction H44. induction H44. unfold TS in H44. spliter. apply False_ind. apply H47. ColR. assumption. unfold Parallelogram_flat in H45. spliter. apply cong_sum; auto. induction H49. left; auto. right; auto. repeat split; Col. Cong. Cong. spliter. subst A'. tauto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg