proposition: Lemma l13_19_par : 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' -> Par_strict X A Y B -> 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 C). subst C. assert(Par A' B' B' C'). apply(par_trans _ _ A B); Par. induction H17. apply False_ind. apply H17. exists B'. split; Col. spliter. assert(A' = C'). apply (l6_21 X A B' A'); Col. intro. apply H13. exists B'. split; Col. subst C'. Par. induction(eq_dec_points B D). subst D. assert(Par A' B' A' D'). apply(par_trans _ _ A B); Par. induction H18. apply False_ind. apply H18. exists A'. split; Col. spliter. assert(B' = D'). apply (l6_21 Y B A' B'); Col. intro. apply H13. exists A'. split; Col. subst D'. Par. induction(eq_dec_points A A'). subst A'. induction H14. apply False_ind. apply H14. exists A. split; Col. spliter. assert(B = B'). apply (l6_21 Y B A B); Col. intro. apply H13. exists A. split; Col. subst B'. assert(C = C'). induction H16. apply False_ind. apply H16. exists B. split; Col. spliter. apply (l6_21 X A B C); Col. intro. apply H13. exists B. split; Col. subst C'. assert(D = D'). induction H15. apply False_ind. apply H15. exists A. split; Col. spliter. apply (l6_21 Y B A D); Col. intro. apply H13. exists A. split; Col. subst D'. auto. apply par_reflexivity. intro. subst D. clean_trivial_hyps. apply H13. exists C. split; Col. induction(par_dec C D C' D'). auto. assert(HH:=not_par_one_not_par C D C' D' A B H20). induction HH. eapply (l13_19_par_aux A B C D A' B' C' D' X Y); Col. intro. apply H21. Par. apply par_distincts in H14. spliter. apply par_symmetry. eapply (l13_19_par_aux A' B' C' D' A B C D X Y); sfinish. intro. subst C'. apply H17. apply (l6_21 X A B A); Col. intro. apply H13. exists B. split; Col. assert(Par B C B A). apply(par_trans _ _ A' B'); Par. induction H24. apply False_ind. apply H24. exists B. split; Col. spliter. Col. intro. apply H18. subst D'. assert(Par A D A B). apply(par_trans _ _ A' B'); Par. apply (l6_21 Y B A B); Col. intro. apply H13. exists A. split; Col. induction H24. apply False_ind. apply H24. exists A. split; Col. spliter. Col. unfold Par_strict in H13. spliter. unfold Par_strict. split. apply coplanar_perm_16, col_cop__cop with A; Col. apply coplanar_perm_16, col_cop__cop with B; Col. intro. apply H24. ex_and H25 P. exists P. split. ColR. ColR. intro. apply H21. apply (par_trans _ _ A' B'); Par. Qed.
imports: GeoCoq.Tarski_dev.Ch13_5_Pappus_Pascal