proposition: Lemma l13_19_aux : forall A B C D A' B' C' D' O, ~Col O A B -> A <> A' -> A <> C -> O <> A -> O <> A' -> O <> C -> O <> C' -> O <> B -> O <> B' -> O <> D -> O <> D' -> Col O A C -> Col O A A' -> Col O A C' -> Col O B D -> Col O B B' -> Col O B D' -> ~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) by (exists O; right; left; split; Col). assert(HH:= cop_npar__inter_exists A B C D H20 H16). ex_and HH E. assert(~Par A' B' O E). intro. assert(Par A B O E). apply (par_trans _ _ A' B'); Par. induction H24. apply H24. exists E. split; Col. spliter. apply H. apply (col_transitivity_1 _ E); Col. assert(Coplanar A' B' O E). apply coplanar_pseudo_trans with O A B; Cop. assert(HH:= cop_npar__inter_exists A' B' O E H24 H23). ex_and HH E'. assert(C <> E). intro. subst E. apply H. apply col_permutation_2. apply (col_transitivity_1 _ C); Col. induction(col_dec A D E). assert(B = D). apply(l6_21 O B A E); Col. intro. subst E. apply H. assert(Col A O D). apply (col_transitivity_1 _ C); Col. apply (col_transitivity_1 _ D); Col. subst D. assert(Par A' B' A' D'). apply (par_trans _ _ A B); Par. induction H29. apply False_ind. apply H29. exists A'. split; Col. spliter. assert(B' = D'). eapply(l6_21 A' B' O B'); Col. intro. apply H. apply (col_transitivity_1 _ A'); Col. apply (col_transitivity_1 _ B'); Col. apply (col_transitivity_1 _ B); Col. subst D'. Par. assert(B <> B'). intro. subst B'. induction H17. apply H17. exists B. split; Col. spliter. apply H. apply col_permutation_2. apply (col_transitivity_1 _ A'); Col. assert(Par D E D' E'). apply (l13_15 A _ _ A' _ _ O); Col. exists B; left; split; Col. induction H18. auto. spliter. apply False_ind. assert(Col A' A D). apply (col_transitivity_1 _ D'); Col. assert(Col A O D). apply (col_transitivity_1 _ A'); Col. apply H. apply (col_transitivity_1 _ D); Col. assert(Par A E A' E'). apply(par_col_par_2 _ B); Col. intro. subst E. apply H28. Col. apply par_symmetry. apply(par_col_par_2 _ B'); Col. intro. subst E'. assert(Col O A E). apply(col_transitivity_1 _ A'); Col. apply H. apply col_permutation_2. apply(col_transitivity_1 _ E); Col. intro. subst E. apply H28. Col. Par. induction H30. auto. spliter. apply False_ind. assert(Col A' A E). apply(col_transitivity_1 _ E'); Col. assert(Col A O E). apply(col_transitivity_1 _ A'); Col. apply H. apply col_permutation_2. apply(col_transitivity_1 _ E); Col. apply(col_transitivity_1 _ B); Col. apply par_comm. induction(col_dec B C E). assert(B = D). apply(l6_21 O B C E); Col. intro. apply H. apply (col_transitivity_1 _ C); Col. subst D. assert(Par A' B' A' D'). apply (par_trans _ _ A B); Par. induction H32. apply False_ind. apply H32. exists A'. split; Col. spliter. assert(B' = D'). eapply(l6_21 A' B' O B'); Col. Col5. ColR. subst D'. Par. assert(Par C E C' E'). apply (l13_15 B _ _ B' _ _ O); Col. exists D; right; left; split; Col. induction H19. auto. spliter. apply False_ind. apply H. assert(Col B O C'). apply (col_transitivity_1 _ B'); Col. apply (col_transitivity_1 _ C'); Col. assert(Par B E B' E'). apply (par_col_par_2 _ A); Col. intro. subst E. apply H31. Col. apply par_symmetry. apply (par_col_par_2 _ A'); Col. intro. subst E'. assert(Col O B E). apply (col_transitivity_1 _ B'); Col. apply H. apply col_permutation_1. apply (col_transitivity_1 _ E); Col. intro. subst E. apply H31. Col. Par. induction H32. auto. spliter. apply False_ind. apply H. assert(Col O B' E'). apply col_permutation_2. apply (col_transitivity_1 _ B); Col. assert(Col B' A' O). apply (col_transitivity_1 _ E'); Col. apply (col_transitivity_1 _ A'); Col. apply (col_transitivity_1 _ B'); Col. apply (col_transitivity_1 _ A); Col. apply(par_col_par_2 _ E); Col. intro. subst D. apply H. apply(col_transitivity_1 _ C); Col. apply par_symmetry. apply(par_col_par_2 _ E'); Col. intro. subst D'. apply H. apply(col_transitivity_1 _ C'); Col. apply (col_par_par_col D E C); Par. Col. Par. Qed.
imports: GeoCoq.Tarski_dev.Ch13_5_Pappus_Pascal