proposition: Lemma l13_19_par_aux : forall A B C D A' B' C' D' X Y, X <> A -> X <> A' -> X <> C -> X <> C' -> Y <> B -> Y <> B' -> Y <> D -> Y <> D' -> Col X A C -> Col X A A' -> Col X A C' -> Col Y B D -> Col Y B B' -> Col Y B D' -> A <> C -> B <> D -> A <> A' -> Par_strict X A Y B -> ~Par A B C D -> Par A B A' B' -> Par A D A' D' -> Par B C B' C' -> Par C D C' D'.
proof: Proof. intros. assert(Coplanar A B C D). apply coplanar_perm_2, col_cop__cop with Y; Col. apply coplanar_perm_16, col_cop__cop with X; Col; Cop. assert(HH := cop_npar__inter_exists A B C D H21 H17). ex_and HH E. assert(HH:= parallel_existence1 X A E H). ex_and HH Z. assert(~Par A B E Z). intro. assert(Par Y B E Z). apply (par_trans _ _ X A); Par. induction H25. apply H25. exists E. split; Col. spliter. induction H24. apply H24. exists A. split; Col. spliter. induction H26. apply H26. exists B. split; Col. spliter. apply H16. exists E. split;ColR. assert(~Par A' B' E Z). intro. apply H25. apply (par_trans _ _ A' B'); Par. assert(Coplanar A' B' E Z). induction H24. CopR. spliter. exfalso. apply H25. right. assert_diffs. repeat split; auto. assert (A <> E). intro. subst E. apply H16. exists D; split; ColR. ColR. assert(HH:= cop_npar__inter_exists A' B' E Z H27 H26). ex_and HH E'. assert(~Col A D E). intro. induction (eq_dec_points A E). subst E. apply H13. apply (l6_21 X A D A); Col. intro. apply H16. exists D. split; Col. apply par_distincts in H19. spliter. auto. assert(Col A B D) by ColR. apply H16. exists A. split; Col. ColR. assert(Par_strict X A E Z). induction H24. Par. spliter. apply False_ind. assert(Col E X A) by ColR. assert(Col A C E) by ColR. apply H13. apply (l6_21 A E D C); Col. intro. subst D. contradiction. apply col_permutation_2. apply (col_transitivity_1 _ E); Col. intro. subst E. clean_trivial_hyps. apply H16. exists B. split; Col. apply col_permutation_1. apply (col_transitivity_1 _ C); Col. assert(Par Y B E Z). apply (par_trans _ _ X A); Par. assert(Par_strict Y B E Z). induction H32. Par. spliter. apply False_ind. assert(Col E Y B) by ColR. assert(Col B D E) by ColR. apply H14. apply (l6_21 B E C D); Col. intro. apply H16. exists C. split; Col. apply col_permutation_1. apply (col_transitivity_1 _ E); Col. intro. subst E. apply H16. exists C. split; Col. clean_trivial_hyps. apply col_permutation_1. apply (col_transitivity_1 _ D); Col. intro. subst D. apply H16. exists C. split; Col. ColR. assert(~Col A' D' E'). intro. assert(Col A' B' D'). apply (col_transitivity_1 _ E'); Col. intro. subst E'. apply H31. exists A'. split; Col. apply H16. exists A'. split; Col. assert(Col Y B' D'). apply (col_transitivity_1 _ B); Col. assert(Col B' A' Y). apply (col_transitivity_1 _ D'); Col. intro. subst D'. assert(Par A D A B). apply(par_trans _ _ A' B'); Par. induction H37. apply H37. exists A. split; Col. spliter. apply H16. exists A. split; Col. apply col_permutation_1. apply (col_transitivity_1 _ D); Col. apply col_permutation_2. apply (col_transitivity_1 _ B'); Col. assert(~ Col X A B). intro. apply H16. exists B. split; Col. assert(~ Col Y A B). intro. apply H16. exists A. split; Col. assert(B <> B'). intro. subst B'. apply H15. apply(l6_21 X A B A); Col. intro. subst B. apply H35. Col. induction H18. apply False_ind. apply H18. exists B. split; Col. spliter. Col. assert(C <> C'). intro. subst C'. induction H20. apply H20. exists C. split; Col. spliter. apply H16. exists C. split; Col. apply col_permutation_1. apply (col_transitivity_1 _ B'); Col. assert(D <> D'). intro. subst D'. induction H19. apply H19. exists D. split; Col. spliter. apply H16. exists D. split; Col. apply col_permutation_1. apply (col_transitivity_1 _ A'); Col. assert(A' <> C'). intro. subst C'. assert(Par B C A B). apply (par_trans _ _ A' B'); Par. induction H40. apply H40. exists B. split; Col. spliter. apply H16. exists B. split; ColR. assert(B' <> D'). intro. subst D'. assert(Par A D A B). apply (par_trans _ _ A' B'); Par. induction H41. apply H41. exists A. split; Col. spliter. apply H16. exists A. split; Col. apply col_permutation_1. apply (col_transitivity_1 _ D); Col. assert(A <> E). intro. subst E. apply H30. Col. assert(A' <> E'). intro. subst E'. apply H34. Col. assert(B <> E). intro. subst E. apply H33. exists B. split; Col. assert(B' <> E'). intro. subst E'. apply H33. exists B'. split; Col. assert(Par A E A' E'). apply (par_col_par_2 _ B); Col. apply par_symmetry. apply (par_col_par_2 _ B'); Col. Par. assert(Par_strict A E A' E'). induction H46. Par. spliter. apply False_ind. apply H47. apply (l6_21 X A' B' E'); Col. intro. apply H16. exists B'. split; Col. apply col_permutation_2. apply (col_transitivity_1 _ A'); Col. apply col_permutation_2. apply (col_transitivity_1 _ A); Col. assert(Par D E D' E'). apply(l13_15_par A D E A' D' E'); Par. induction H19. Par. spliter. apply False_ind. apply H16. exists D. split; Col. apply col_permutation_1. apply (col_transitivity_1 _ A'); Col. apply col_permutation_2. apply (col_transitivity_1 _ D'); Col. apply (par_col_par_2 _ X); Col. apply par_symmetry. apply (par_col_par_2 _ Y); Col. apply col_permutation_2. apply (col_transitivity_1 _ B); Col. apply par_comm. apply (par_col_par_2 _ B); Col. apply (par_trans _ _ E Z); Par. apply (par_col_par_2 _ X); Par; Col. apply par_symmetry. apply (par_col_par_2 _ Z); Col. intro. subst E'. apply H47. exists E. split; Col. Par. assert(Par C E C' E'). eapply(l13_15_par B C E B' C' E'); Par. intro. assert(Col B A C) by ColR. apply H16. exists B. split; ColR. induction H20. Par. spliter. apply False_ind. apply H16. exists B'. split; Col. assert(Col X C C'). apply (col_transitivity_1 _ A); Col. assert(Col C B' X). apply (col_transitivity_1 _ C'); Col. apply col_permutation_2. apply (col_transitivity_1 _ C); Col. assert(Par B E B' E'). apply (par_col_par_2 _ A); Col. apply par_symmetry. apply (par_col_par_2 _ A'); Col. Par. induction H49. Par. spliter. apply False_ind. assert(Col B' A' B) by ColR. apply H16. exists A'. split; ColR. apply (par_col_par_2 _ Y); Col. apply par_symmetry. apply (par_col_par_2 _ X); Col. apply col_permutation_2. apply (col_transitivity_1 _ A); Col. apply par_left_comm. apply (par_col_par_2 _ A); Col. apply (par_trans _ _ E Z); Par. apply (par_col_par_2 _ Y); Col. apply par_symmetry. apply (par_col_par_2 _ Z); Col. intro. subst E'. apply H47. exists E. split; Col. Par. apply (par_col_par_2 _ E); Col. intro. subst D. apply H16. exists C. split; Col. apply par_symmetry. apply (par_col_par_2 _ E'); Col. intro. subst D'. apply H16. exists C'. split; Col. apply (col_par_par_col C E D); Col ; Par. Par. Qed.
imports: GeoCoq.Tarski_dev.Ch13_5_Pappus_Pascal