proposition: Lemma l13_15_1 : forall A B C A' B' C' O, ~ Col A B C -> ~ Par O B A C -> Coplanar 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 B A' B'). intro. apply H2. exists B. split; Col. assert(~Col A A' B'). intro. apply H2. exists A. split; Col. assert(B <> O). intro. subst B. apply H2. exists A'. split; Col. assert(A <> O). intro. subst A. apply H2. exists B'. split; Col. assert(~ Col A' A C). eapply (par_not_col A' C'). Par. Col. assert(C <> O). intro. subst C. apply H11. Col. assert(~Col O A B). intro. apply H2. exists O. split. Col. assert(Col O A B'). apply (col_transitivity_1 _ B); Col. apply (col_transitivity_1 _ A); Col. assert(~Col O A C). intro. apply H3. exists O. split. Col. assert(Col O A C'). apply (col_transitivity_1 _ C); Col. apply (col_transitivity_1 _ A); Col. assert(~ Col A' B' C'). intro. apply H. assert(Par A' C' A B). apply(par_col_par_2 A' B' A B C'). apply par_strict_distinct in H3. spliter. auto. auto. left. Par. assert(Par A C A B). apply(par_trans A C A' C'); Par. induction H17. apply False_ind. apply H17. exists A. split; Col. spliter; Col. induction(col_dec O B C). right. repeat split. intro. subst C. apply H. Col. intro. subst C'. apply H15. Col. assert(Col O B C'). apply (col_transitivity_1 _ C); Col. apply (col_transitivity_1 _ O); Col. assert(Col O C B'). apply (col_transitivity_1 _ B); Col. apply (col_transitivity_1 _ O); Col. assert(B' <> O). intro. subst B'. apply H8. Col. assert(B' <> O). intro. subst B'. apply H8. Col. assert(A' <> O). intro. subst A'. apply H7. Col. assert(~ Col A A' C'). apply (par_not_col A C). Par. Col. assert(C' <> O). intro. subst C'. apply H20. Col. assert(~Col O A' B'). intro. apply H2. exists O. split. assert(Col O A' B). apply (col_transitivity_1 _ B'); Col. apply (col_transitivity_1 _ A'); Col. Col. assert(~Col O A' C'). intro. apply H3. exists O. split. ColR. Col. assert(~Col B' A B). intro. apply H2. exists B'. Col. assert(~Col A' A B). intro. apply H2. exists A'. split; Col. assert(exists C : Tpoint, exists D : Tpoint, C <> D /\ Par O B C D /\ Col A C D). apply(parallel_existence O B A). auto. ex_and H26 X. ex_and H27 Y. assert(Coplanar O B X A) by (apply col_cop__cop with Y; Col; Cop). assert(Coplanar O B Y A) by (apply col_cop__cop with X; Col; Cop). assert(exists L : Tpoint, Col L X Y /\ Col L A' C'). apply(cop_npar__inter_exists X Y A' C'). apply coplanar_pseudo_trans with O A B; [Cop..|]. apply coplanar_perm_12, col_cop__cop with C; Cop. intro. apply H0. eapply (par_trans O B X Y). auto. apply par_symmetry. apply (par_trans A C A' C'). left. auto. Par. ex_and H31 L. assert(A <> L). intro. subst L. contradiction. assert(Par A L O B'). apply par_symmetry. apply(par_col_par_2 _ B); Col. apply par_symmetry. apply par_left_comm. induction(eq_dec_points X L). subst X. apply (par_col_par_2 _ Y); Col. Par. apply (par_col_par_2 _ X); try auto. ColR. apply par_left_comm. apply (par_col_par_2 _ Y); Col. Par. assert(~ Par X Y O C). intro. assert(Par O B O C). apply (par_trans O B X Y); Par. induction H36. apply H36. exists O. split; Col. spliter. apply H16. Col. assert(Coplanar X Y O C). apply coplanar_pseudo_trans with O A B; Cop. assert(HH:=cop_npar__inter_exists X Y O C H36 H35). ex_and HH M. assert(A <> M). intro. subst M. apply H14. Col. assert(Par O B A M). apply (par_col_par_2 _ B'); Col. apply par_symmetry. apply (par_col_par_2 _ L); try auto. ColR. assert(L <> A'). intro. subst L. clean_trivial_hyps. apply H13. induction(eq_dec_points A' X). subst X. assert(Par A' A O B). apply (par_col_par_2 _ Y); Col. Par. induction H32. apply False_ind. apply H32. exists O. split; Col. spliter. ColR. assert(Par X A' O B). apply (par_col_par_2 _ Y); Col. Par. assert(Par A' A O B). apply (par_col_par_2 _ X); try auto. ColR. Par. induction H42. apply False_ind. apply H42. exists O. split; Col. spliter. Col. assert(~ Par L B' A' B'). intro. induction H42. apply H42. exists B'. split;Col. spliter. apply H15. eapply (col_transitivity_1 _ L); Col. assert(~ Par A B L B'). apply(par_not_par A' B' A B L B'). left. Par. intro. apply H42. Par. assert(Coplanar A B L B'). apply coplanar_perm_4, col_cop__cop with O; Col; Cop. assert(HH:=cop_npar__inter_exists A B L B' H44 H43). ex_and HH N. assert(Par_strict A L O B'). induction H34. auto. spliter. apply False_ind. apply H13. apply (col_transitivity_1 _ B'); Col. assert(A <> N). intro. subst N. apply H47. exists B'; Col. assert(Par A N A' B'). apply (par_col_par_2 _ B); Col. left. Par. clean_duplicated_hyps. assert(Par O N L A'). induction(par_dec A O N L). assert(Par_strict A O N L). induction H18. auto. spliter. apply False_ind. apply H24. assert(Col N A B'). eapply (col_transitivity_1 _ L); Col. apply col_permutation_2. eapply (col_transitivity_1 _ N); Col. apply(l13_14 A O A' A N L N B'); Col. Par. Par. assert(N <> L). intro. subst L. apply H47. exists B. split; Col. assert(Coplanar A O N L). assert_diffs; apply coplanar_perm_1, col_cop__cop with B'; Col; Cop. assert(HH:=cop_npar__inter_exists A O N L H51 H18). ex_and HH P. apply par_right_comm. assert(P <> L). intro. subst P. apply H47. exists O. split; Col. assert(P <> O). intro. subst P. apply H47. exists L. split. Col. apply (col_transitivity_1 _ N); Col. assert(L <> B'). intro. subst L. apply H47. exists B'. split; Col. assert(A <> P). intro. subst P. assert(Col A B L). apply (col_transitivity_1 _ N); Col. assert(Col L A B'). apply (col_transitivity_1 _ N); Col. apply H43. apply par_symmetry. right. repeat split. assumption. intro. subst B. apply H24. Col. Col. ColR. assert(P <> N). intro. subst P. apply H13. apply col_permutation_2. apply (col_transitivity_1 _ N); Col. assert(A' <> P). intro. subst P. apply H42. right. repeat split; try assumption. intro. subst B'. apply H22. Col. ColR. Col. assert(B' <> P). intro. subst P. apply H22. apply (col_transitivity_1 _ A); Col. apply(l13_11 O A' A L N B' P); Par; try ColR. intro. apply H47. exists L. split. Col. assert(Col L O N). apply (col_transitivity_1 _ P); Col. apply (col_transitivity_1 _ N); Col. assert(Par A' C' O N). apply (par_col_par_2 _ L). intro. subst C'. apply H23. Col. Col. Par. assert(Par O N A C). apply (par_trans _ _ A' C'); Par. assert(Par N M B C). induction(par_dec A N O C). assert(Par_strict A N O C). induction H52. auto. spliter. apply False_ind. apply H14. Col. apply par_right_comm. apply(l13_14 A N B A O C M O ); Par; Col. assert(Coplanar A N O C) by Cop. assert(HH:= cop_npar__inter_exists A N O C H53 H52). ex_and HH P. assert(B <> P). intro. subst P. apply H16. Col. assert(A <> P). intro. subst P. apply H14. Col. assert(M <> P). intro. subst P. induction H40. apply H40. exists B. split. Col. apply col_permutation_2. apply (col_transitivity_1 _ N); Col. spliter. apply H13. apply col_permutation_2. apply (col_transitivity_1 _ M); Col. assert(O <> P). intro. subst P. induction H51. apply H51. exists A. split; Col. spliter. apply H14. Col. assert(P <> N). intro. subst P. induction H51. apply H51. exists C. split; Col. spliter. apply H14. Col. apply(l13_11 N B A C M O P); Par; try ColR. intro. assert(Col N A C) by ColR. apply H. ColR. assert(Par N M B' C'). induction(par_dec N B' O C'). assert(Par_strict N B' O C'). induction H53. auto. spliter. apply False_ind. induction H51. apply H51. exists C. split. ColR. Col. spliter. contradiction. assert(M <> L). intro. subst M. apply H54. exists L. split. Col. apply col_permutation_2. apply(col_transitivity_1 _ C); Col. assert(L <> C'). intro. subst C'. apply H54. exists L. split; Col. assert(Par L M O B'). apply (par_col_par_2 _ A); try assumption. auto. ColR. Par. assert(Par L C' O N). apply (par_col_par_2 _ A'); Col. Par. apply par_right_comm. apply(l13_14 B' N B' L O C' M O); Par; ColR. assert(Coplanar N B' O C'). apply coplanar_pseudo_trans with O A B; [Cop..|]. apply coplanar_perm_12, col_cop__cop with C; Col; Cop. assert(HH:= cop_npar__inter_exists N B' O C' H54 H53). ex_and HH P. assert(B' <> P). intro. subst P. apply H16. ColR. induction(eq_dec_points C' L). subst L. assert(C' = M). induction (col_dec O X C). apply (l6_21 O C Y X). intro. assert(Col O X Y) by ColR. induction H27. apply H27. exists O. split; Col. spliter. apply H13. apply(col3 X Y); Col. auto. Col. Col. Col. Col. apply (l6_21 O C X Y); Col. subst M. right. repeat split; auto. apply par_distincts in H52; spliter; auto. intro; subst; apply H15; Col. Col. Col. assert(L <> P). intro. subst P. apply H23. apply col_permutation_1. apply (col_transitivity_1 _ L); Col. induction (eq_dec_points L M). subst L. assert(C' = M). apply (l6_21 O C A' C'); Col. intro. apply H23. ColR. intro. subst C'. apply H23. Col. subst M. right. repeat split; auto. Col. Col. assert(Par L M O B'). apply (par_col_par_2 _ A); try assumption. ColR. Par. assert(Par L C' N O). apply (par_col_par_2 _ A'); Col. Par. assert(B' <> N). intro. subst N. contradiction. apply(l13_11 N B' L C' M O P); Par. intro. assert(Col P B' C'). apply (col_transitivity_1 _ N). intro. subst N. induction H50. apply H50. exists C'. split; Col. spliter. apply H23. ColR. Col. Col. assert(Col C' O B' ). apply (col_transitivity_1 _ P). intro. subst P. clean_trivial_hyps. assert(Col B' C' L). apply (col_transitivity_1 _ N); Col. apply H15. ColR. Col. Col. assert(Col O B C'). apply (col_transitivity_1 _ B'); Col. apply H16. ColR. ColR. intro. subst M. assert(Col B' P L). apply (col_transitivity_1 _ N); Col. assert(Col L A B'). assert(Col P A L). apply (col3 X Y); Col. apply (col_transitivity_1 _ P); Col. apply H47. exists B'. split; Col. intro. subst P. assert(N = B). apply (l6_21 A B O B'); Col. subst N. induction H52. apply H52. exists B. split; Col. spliter. assert(B = O). apply (l6_21 O B' M C); Col. subst B. induction H61. apply H61. exists L. split; Col. tauto. ColR. ColR. apply (par_trans _ _ N M); Par. Qed.
imports: GeoCoq.Tarski_dev.Ch13_5_Pappus_Pascal