proposition: Lemma l13_15_2_aux : forall A B C A' B' C' O , ~Col A B C -> ~Par O A B C -> Par O B A C -> Par_strict A B A' B' -> Par_strict A C A' C' -> Col O A A' -> Col O B B' -> Col O C C' -> Par B C B' C'.
proof: Proof. intros. assert(~Col O A B /\ ~Col O B C /\ ~Col O A C). induction H1; repeat split; intro. apply H1. exists A. split; Col. apply H1. exists C. split; Col. apply H1. exists O. split; Col. spliter. apply H; Col. spliter. apply H; Col. spliter. apply H; Col. spliter. assert( A <> O /\ B <> O /\ C <> O). repeat split; intro; subst O. apply H9. Col. apply H8. Col. apply H9. Col. spliter. assert( A' <> O). intro. subst A'. assert(Par O B A B). apply (par_col_par_2 _ B'); Col. left. Par. induction H13. apply H13. exists B. split; Col. spliter. contradiction. assert(B' <> O). intro. subst B'. assert(Par O A B A). apply(par_col_par_2 _ A'); Col. apply par_comm. apply par_symmetry. left. Par. induction H14. apply H14. exists A. split; Col. spliter. apply H7. Col. assert(C' <> O). intro. subst C'. assert(Par O A C A). apply (par_col_par_2 _ A'); Col. apply par_comm. apply par_symmetry. left. Par. induction H15. apply H15. exists A. split; Col. spliter. apply H9. Col. assert(~Col O A' B'). intro. assert(Col O A B'). apply (col_transitivity_1 _ A'); Col. apply H7. apply (col_transitivity_1 _ B'); Col. assert(~Col O B' C'). intro. assert(Col O B C'). apply (col_transitivity_1 _ B'); Col. apply H8. apply (col_transitivity_1 _ C'); Col. assert(~Col O A' C'). intro. assert(Col O A C'). apply (col_transitivity_1 _ A'); Col. apply H9. apply (col_transitivity_1 _ C'); Col. assert(A <> A'). intro. subst A'. apply H3. exists A. split; Col. assert(B <> B'). intro. subst B'. apply H2. exists B. split; Col. assert(C <> C'). intro. subst C'. apply H3. exists C. split; Col. induction(par_dec B C B' C'). auto. assert(B <> C). intro. subst C. apply H. Col. assert(HP:=parallel_existence B C B' H23). ex_and HP X. ex_and H24 Y. assert(~Par X Y O C). intro. assert(Par O C B C). apply (par_trans _ _ X Y); Par. induction H28. apply H28. exists C. split; Col. spliter. contradiction. assert(Coplanar X Y O C). induction H25. apply coplanar_pseudo_trans with B C B'. apply not_col_permutation_1, (par_not_col X Y); Par. apply coplanar_perm_1, col_cop__cop with Y; Col; Cop. apply coplanar_perm_1, col_cop__cop with X; Col; Cop. Cop. Cop. spliter. Cop. assert(HH:=cop_npar__inter_exists X Y O C H28 H27). ex_and HH C''. assert(B' <> C''). intro. subst C''. assert(Col O B C). apply (col_transitivity_1 _ B'); Col. contradiction. assert(Par B' C'' B C ). induction(eq_dec_points B' X). subst X. apply (par_col_par_2 _ Y). auto. Col. Par. apply (par_col_par_2 _ X). auto. apply col_permutation_2. apply(col_transitivity_1 _ Y); Col. apply par_left_comm. apply (par_col_par_2 _ Y); Col. Par. assert(Par A C A' C''). apply(l13_15_1 B A C B' A' C'' O); Col. Cop. apply par_strict_comm. auto. induction H32. Par. spliter. apply False_ind. apply H8. apply col_permutation_2. apply(col_transitivity_1 _ B'); Col. assert(C' <> C''). intro. subst C''. apply H22. Par. assert(Par A' C' A' C''). apply (par_trans _ _ A C). left. Par. Par. assert(C' = C''). apply (l6_21 A' C' O C); Col. induction H35. apply False_ind. apply H35. exists A'. split; Col. spliter. Col. contradiction. Qed.
imports: GeoCoq.Tarski_dev.Ch13_5_Pappus_Pascal