proposition: Lemma cong_sum : forall A B C, O <> C \/ B <> A -> Ar2 O E E' A B C -> Cong O A B C -> Cong O B A C -> Sum O E E' A B C.
proof: Proof. intros A B C. intro Hor. intros. induction (eq_dec_points A O). subst A. unfold Ar2 in H. spliter. apply cong_symmetry in H0. apply cong_identity in H0. subst C. apply sum_O_B; Col. induction (eq_dec_points B O). subst B. unfold Ar2 in H. spliter. apply cong_symmetry in H1. apply cong_identity in H1. subst C. apply sum_A_O; Col. unfold Sum. split; auto. unfold Ar2 in H. assert(HH:=grid_not_par). spliter. assert(exists ! P' : Tpoint, Proj A P' O E' E E'). apply(project_existence A O E' E E'); auto. intro. apply H6. Par. ex_and H13 A'. unfold unique in H14. spliter. clear H14. unfold Proj in H13. spliter. clean_duplicated_hyps. assert(HH:=parallel_existence1 O E A' H7). ex_and HH P'. assert(exists ! C' : Tpoint, Proj B C' A' P' O E'). apply(project_existence B A' P' O E'); auto. apply par_distincts in H. spliter. auto. intro. apply H5. apply(par_trans _ _ A' P'); Par. ex_and H13 C'. unfold unique in H14. spliter. clear H14. unfold Proj in H13. spliter. exists A'. exists C'. assert(A' <> O). intro. subst A'. induction H17. induction H17. apply H17. exists E. split; Col. spliter. contradiction. contradiction. assert(Par_strict O E A' P'). unfold Par_strict. repeat split; auto; try apply all_coplanar. intro. ex_and H21 X. induction H. apply H. exists X. split; Col. spliter. apply grid_ok. ColR. assert(A <> A'). intro. subst A'. apply H21. exists A. split; Col. repeat split; Col. induction H17. left; Par. right; auto. left. apply (par_col_par _ _ _ P'). intro. subst C'. induction H19. induction H19. apply H19. exists A'. split; Col. spliter. apply grid_ok. ColR. subst A'. apply H21. exists B. split; Col. Par. Col. induction H19. left. Par. right. auto. assert(A' <> C'). intro. subst C'. induction H19. induction H19. apply H19. exists A'. split; Col. spliter. apply grid_ok. ColR. subst A'. apply H21. exists B. split; Col. assert(Plg O B C' A'). apply(pars_par_plg O B C' A'). apply par_strict_right_comm. apply(par_strict_col_par_strict _ _ _ P'). auto. apply par_strict_symmetry. apply(par_strict_col_par_strict _ _ _ E). auto. Par. Col. Col. induction H19. apply par_symmetry. apply(par_col_par _ _ _ E'). auto. Par. Col. subst C'. apply False_ind. apply H21. exists B. split; Col. assert(Plg O B C A). apply(parallelogram_to_plg). right. unfold Parallelogram_flat. repeat split; try ColR. Cong. Cong. auto. apply plg_to_parallelogram in H24. apply plg_to_parallelogram in H25. assert(Parallelogram A C C' A'). 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_permut. apply plg_permut. assumption. assumption. induction H26. apply plg_comm2. assumption. spliter. subst C'. subst A'. tauto. apply plg_par in H26. spliter. induction H17. left. apply(par_trans _ _ A A'); Par. contradiction. intro. subst C. apply cong_identity in H1. subst B. tauto. intro. subst C'. apply plg_permut in H26. induction H19. induction H19. apply H19. exists O. split; Col. ColR. spliter. apply grid_ok. ColR. subst C. apply H21. exists B. split; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg