proposition: Lemma sum_plg : forall A B C, Sum O E E' A B C -> (A <> O ) \/ ( B <> O) -> exists A', exists C', Plg O B C' A' /\ Plg C' A' A C.
proof: Proof. intros. assert(HS:=H). unfold Sum in H. spliter. ex_and H1 A'. ex_and H2 C'. exists A'. exists C'. unfold Pj in *. unfold Ar2 in H. assert(HH:= grid_not_par). spliter. induction(eq_dec_points O B). subst B. assert(HH:=sum_A_O A H12). assert(HP:=sum_uniqueness A O C A HS HH). subst C. induction H4. induction H4. apply False_ind. apply H4. exists O. split; Col. spliter. induction H3. induction H3. apply False_ind. apply H3. exists O. split. Col. apply (col_transitivity_1 _ E'); Col. spliter. apply False_ind. apply grid_ok. assert(Col C' O E). ColR. ColR. subst C'. split; apply parallelogram_to_plg; apply plg_trivial1. auto. intro. subst A'. apply H. ColR. subst C'. apply False_ind. induction H5. apply H6. apply par_symmetry. apply (par_col_par _ _ _ A); Col; Par. subst A. induction H0; tauto. induction(eq_dec_points A O). subst A. assert(HH:=sum_O_B B H13 ). assert(HP:=sum_uniqueness O B C B HS HH). subst C. clean_trivial_hyps. induction H1. induction H1. apply False_ind. apply H1. exists E'. split; Col. spliter. apply False_ind. apply H. apply (col_transitivity_1 _ A'); Col. subst A'. clean_trivial_hyps. induction H5. induction H4. apply False_ind. apply H8. apply (par_trans _ _ B C'); Par. subst C'. split; apply parallelogram_to_plg; apply plg_trivial; auto. subst C'. split; apply parallelogram_to_plg; apply plg_trivial; auto. assert(A' <> O). intro. subst A'. induction H1. apply H6. apply par_symmetry. apply (par_col_par _ _ _ A); Col;Par. contradiction. assert(A' <> O /\ (Par_strict O E A' C' \/ B = O)). apply(sum_par_strict A B C A' C');auto. repeat split; auto. spliter. induction H19. assert(Par O B C' A'). apply par_symmetry. apply (par_col_par _ _ _ E); Par. assert(Par_strict O B C' A'). induction H20. auto. spliter. apply False_ind. apply H19. exists O. split; Col. induction H4. assert(Par O A' B C'). apply par_symmetry. apply (par_col_par _ _ _ E'); Par; Col. assert(HX:= pars_par_plg O B C' A' H21 H22). assert(Par C' A' A C). apply(par_col_par _ _ _ O). intro. subst C. apply H15. apply sym_equal. apply(sum_A_B_A A); auto. apply par_right_comm. apply(par_col_par _ _ _ B). auto. Par. ColR. ColR. assert(Par_strict C' A' A C). induction H23. auto. spliter. apply False_ind. apply H19. exists C'. split. ColR. Col. induction H1. induction H5. assert(Par C' C A' A). apply (par_trans _ _ E E'); Par. assert(HY:= pars_par_plg C' A' A C H24 H25). split; auto. subst C'. assert_diffs;contradiction. split; Col. subst A'. assert_diffs. contradiction. subst C'. assert_diffs. contradiction. subst B. tauto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg