proposition: Lemma l13_18_2 : forall A B C A' B' C' O, ~Col A B C -> Par_strict A B A' B' -> Par_strict A C A' C' -> (Par_strict B C B' C' /\ Col O A A' /\ Col O B B' -> Col O C C').
proof: Proof. intros. spliter. assert(~ Col O A B). intro. apply H0. exists O. split. Col. apply(col_transitivity_1 _ A); Col. intro. subst A. apply H0. exists B'. split; Col. apply(col_transitivity_1 _ B); Col. intro. subst B. apply H0. exists A'. split; Col. assert(exists X : Tpoint, Col X B' C' /\ Col X O C). apply cop_npar__inter_exists. assert_diffs; apply coplanar_perm_13, col_cop__cop with B; Col; Cop. apply par_not_par with B C; Par. intro. induction H6. apply H6. exists C. split; Col. spliter. apply H2. exists B'. split;Col. apply col_permutation_2. apply (col_transitivity_1 _ O); Col. intro. subst O. apply H0. exists A'. split; Col. ex_and H6 C''. induction(col_dec O C C'). auto. apply False_ind. assert(Par C' C'' B C ). apply (par_col_par_2 _ B'). intro. subst C''. Col. Col. apply par_left_comm. left. Par. assert(Par_strict C' C'' B C). induction H9. auto. spliter. apply False_ind. apply H8. apply col_permutation_2. apply (col_transitivity_1 _ C''). intro. subst C''. apply H2. exists C. split; Col. apply (col_transitivity_1 _ B); Col. Col. assert(~Col O B C). intro. apply H10. exists B'. split; Col. apply col_permutation_2. apply (col_transitivity_1 _ O); Col. intro. subst B. apply H5. Col. assert(Par B' C'' B C). apply (par_col_par_2 _ C') ; Col. intro. subst B'. apply H11. apply(col_transitivity_1 _ C''); Col. intro. subst C''. apply H0. exists A. split; Col. left. Par. assert(Par_strict B' C'' B C). induction H12. auto. spliter. apply False_ind. apply H11. apply col_permutation_2. apply (col_transitivity_1 _ B'); Col. intro. subst B'. apply H2. exists B. split; Col. assert(Par A C A' C''). apply(l13_15 B A C B' A' C'' O); Par; Col. assert_diffs; apply coplanar_perm_3, coplanar_trans_1 with C'; Col. apply coplanar_perm_4, col_cop__cop with A'; Col; Cop. apply coplanar_perm_4, col_cop__cop with B'; Col; Cop. assert(Par A' C' A' C''). apply (par_trans _ _ A C). left. Par. Par. induction H15. apply H15. exists A'. split; Col. spliter. assert(~ Col A' B' C'). intro. apply H. apply(col_par_par_col A' B' C' A B C H19); left; Par. assert( C' = C''). apply(l6_21 A' C' B' C'); Col. intro. subst C'. apply H19. Col. subst C''. Col. Qed.
imports: GeoCoq.Tarski_dev.Ch13_5_Pappus_Pascal