proposition: Lemma change_grid_sum_0 : 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 -> A = O -> Sum O' E' E A' B' C'.
proof: Proof. intros. assert(HS:= H6). induction H6. ex_and H8 A1. ex_and H9 C1. unfold Ar1 in *. unfold Ar2 in H6. spliter. subst A. clean_duplicated_hyps. assert(A' = O'). apply(l6_21 O' E' O O');Col. intro. apply H. exists O. split; Col. intro. apply H. subst O'. exists O. split; Col. unfold Pj in H3. induction H3. induction H3. apply False_ind. apply H3. exists O. split; Col. spliter. Col. subst A'. Col. subst A'. assert(Sum O E E' O B B). apply sum_O_B. assumption. Col. unfold Sum in H7. assert(B = C). apply(sum_uniqueness O E E' O B); auto. subst C. assert(B' = C'). apply(l6_21 O' E' B B'); Col. intro. apply H. exists B. split; Col. intro. subst B'. apply H. exists B. split; Col. induction H5. induction H4. assert(Par B C' B B'). apply(par_trans _ _ O O'); Par. induction H13. apply False_ind. apply H13. exists B. split; Col. spliter. Col. subst B'. Col. subst C'. Col. subst C'. apply sum_O_B;Col. assert_ncols; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg