proposition: Lemma l13_15_2 : forall A B C A' B' C' O , ~Col A B C -> Par 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. induction(par_dec B C B' C'). auto. assert(HH:=not_par_one_not_par B C B' C' O A H6). induction HH. apply (l13_15_2_aux A B C A' B' C' O); auto. intro. apply H7. Par. apply par_symmetry. assert(~ Col A' B' C'). intro. apply H. assert(Par A' B' A' C'). right. repeat split; Col. intro. subst B'. apply H1. exists A. split; Col. intro. subst C'. apply H2. exists A. split; Col. assert(Par A B A C). apply(par_trans _ _ A' B'). left. auto. apply(par_trans _ _ A' C'). Par. left. Par. induction H10. apply False_ind. apply H10. exists A. split; Col. spliter. Col. assert(B' <> O). intro. subst B'. assert(Par O A B A). apply (par_col_par_2 _ A'); Col. intro. subst A. apply H1. exists O. split; Col. apply par_comm. left. Par. induction H9. apply H9. exists A. split; Col. spliter. apply H1. exists O. split; Col. assert(Par O B O B'). right. repeat split; Col. intro. subst B. apply par_distincts in H0. tauto. apply (l13_15_2_aux A' B' C' A B C O); Col; Par. intro. apply H7. apply par_symmetry. apply (par_col_par_2 _ A'). intro. subst A. induction H0. apply H0. exists O. split; Col. spliter. apply H. Col. Col. Par. apply (par_trans _ _ O B). Par. apply (par_trans _ _ A C). Par. left. Par. Qed.
imports: GeoCoq.Tarski_dev.Ch13_5_Pappus_Pascal