proposition: Lemma opp_exists : forall A, Col O E A -> exists MA, Opp O E E' A MA.
proof: Proof. intros. assert(NC:= grid_ok). induction(eq_dec_points A O). subst A. exists O. unfold Opp. unfold Sum. split. unfold Ar2. repeat split; Col. exists O. exists O. repeat split; Col; try right; auto. prolong A O MA A O. exists MA. unfold Opp. apply sump_to_sum. unfold Sump. repeat split. apply bet_col in H1. apply (col_transitivity_1 _ A);Col. Col. assert(E <> E' /\ O <> E'). split; intro; subst E'; apply NC; Col. spliter. assert(exists! P' : Tpoint, Proj MA P' O E' E E'). apply(project_existence MA O E' E E'); auto. intro. induction H5. apply H5. exists E'. split; Col. spliter. apply NC. Col. ex_and H5 A'. unfold unique in H6. spliter. exists A'. assert(O <> E). intro. subst E. apply NC. Col. assert(HH:= parallel_existence1 O E A' H7). ex_and HH P'. assert(exists! C' : Tpoint, Proj A C' A' P' O E'). apply(project_existence A A' P' O E'); auto. apply par_distincts in H8. spliter. auto. intro. assert(Par O E O E'). apply (par_trans _ _ A' P'). auto. apply par_symmetry; auto. induction H10. apply H10. exists O. split; Col. spliter. apply NC. Col. ex_and H9 C'. unfold unique in H10. spliter. exists C'. exists P'. split; auto. split; auto. split; auto. unfold Proj in H5. spliter. unfold Proj. repeat split; Col. intro. induction H15. apply H15. exists E. split; Col. apply NC. tauto. left. unfold Proj in H9. spliter. assert(Par O E' O A'). right. repeat split; Col. intro. subst A'. clean_trivial_hyps. induction H14. induction H13. apply H13. exists E. split; Col. apply col_permutation_1. apply bet_col in H1. apply(col_transitivity_1 _ A); Col. apply NC. tauto. subst MA. apply cong_symmetry in H2. apply cong_identity in H2. contradiction. assert(Plg A C' A' O). apply pars_par_plg. induction H18. assert(Par A C' A' O). apply (par_trans _ _ O E'). Par. Par. induction H20. auto. spliter. apply False_ind. apply NC. apply (col_transitivity_1 _ A'); Col. apply (col_transitivity_1 _ A); Col. subst C'. apply False_ind. induction H8. apply H8. exists A. split; Col. spliter. apply NC. apply (col_transitivity_1 _ A'); Col. intro. subst A'. apply par_distincts in H19. tauto. apply col_permutation_2. apply (col_transitivity_1 _ P'); Col. apply par_comm. apply (par_col_par _ _ _ P'). intro. subst C'. induction H18. induction H18. apply H18. exists A'. split; Col. spliter. apply NC. apply (col_transitivity_1 _ A); Col. subst A'. induction H19. apply H18. exists O. split; Col. spliter. apply NC. apply (col_transitivity_1 _ A); Col. apply par_symmetry. apply (par_col_par _ _ _ E); Col. apply par_symmetry. Par. Col. assert(Parallelogram A O MA O). right. unfold Parallelogram_flat. repeat split; Col; Cong. left. intro. subst MA. apply between_identity in H1. contradiction. apply plg_to_parallelogram in H20. apply plg_permut in H20. apply plg_comm2 in H21. assert(Parallelogram C' A' MA O). assert(HH:= plg_pseudo_trans C' A' O A O MA H20 H21). induction HH. auto. spliter. subst MA. apply cong_symmetry in H2. apply cong_identity in H2. contradiction. apply plg_par in H22. spliter. induction H14. apply (par_trans _ _ A' MA). auto. Par. subst MA. apply par_distincts in H23. tauto. intro. subst C'. unfold Parallelogram in H20. induction H20. unfold Parallelogram_strict in H20. spliter. apply par_distincts in H23. tauto. unfold Parallelogram_flat in H20. spliter. apply cong_symmetry in H24. apply cong_identity in H24. subst A. tauto. intro. subst MA. unfold Parallelogram in H21. induction H21. unfold Parallelogram_strict in H21. spliter. unfold TS in H21; unfold Parallelogram. spliter; Col. unfold Parallelogram_flat in H21. spliter. apply NC. apply (col_transitivity_1 _ A); Col. apply (col_transitivity_1 _ A'); Col. intro. subst A'. apply cong_identity in H24. subst A. tauto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg