proposition: Lemma l13_19 : forall A B C D A' B' C' D' O, ~Col O A B -> 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 A' B' -> Par A D A' D' -> Par B C B' C' -> Par C D C' D'.
proof: Proof. intros. induction (eq_dec_points A A'). subst A'. assert(B = B'). apply(l6_21 A B O B); Col. induction H14. apply False_ind. apply H14. exists A. split; Col. spliter. Col. subst B'. assert(D = D'). apply(l6_21 A D O B); Col. intro. apply H. apply (col_transitivity_1 _ D); Col. induction H15. apply False_ind. apply H15. exists A. split; Col. spliter. Col. subst D'. assert(C = C'). apply(l6_21 B C O A); Col. intro. apply H. apply (col_transitivity_1 _ C); Col. induction H16. apply False_ind. apply H16. exists B. split; Col. spliter. Col. subst C'. apply par_reflexivity. intro. subst D. apply H. apply (col_transitivity_1 _ C); Col. induction(eq_dec_points A C). subst C. assert(A' = C'). assert(Par A' B' B' C'). apply (par_trans _ _ A B); Par. induction H18. apply False_ind. apply H18. exists B'. split; Col. spliter. eapply (l6_21 B' C' O A); Col. intro. apply H. apply (col_transitivity_1 _ B'); Col. apply (col_transitivity_1 _ C'); Col. subst C'. auto. induction(eq_dec_points A' C'). subst C'. assert(A = C). assert(Par A B B C). apply (par_trans _ _ A' B'); Par. induction H19. apply False_ind. apply H19. exists B. split; Col. spliter. eapply (l6_21 B C O A'); Col. intro. apply H. apply (col_transitivity_1 _ C); Col. apply (col_transitivity_1 _ A); Col. contradiction. induction(par_dec C D C' D'). auto. assert(HH:=not_par_one_not_par C D C' D' A' B' H20). induction HH. assert(~ Par C D A B). intro. apply H21. apply (par_trans _ _ A B); Par. apply (l13_19_aux A B C D A' B' C' D' O); Col. intro. apply H21. apply (par_trans _ _ A B); Par. apply par_symmetry. apply (l13_19_aux A' B' C' D' A B C D O); Par. intro. apply H. apply (col_transitivity_1 _ A'); Col. apply (col_transitivity_1 _ B'); Col. apply (col_transitivity_1 _ A); Col. Col. apply (col_transitivity_1 _ A); Col. apply (col_transitivity_1 _ B); Col. Col. apply (col_transitivity_1 _ B); Col. Qed.
imports: GeoCoq.Tarski_dev.Ch13_5_Pappus_Pascal