proposition: Lemma l13_18_3 : forall A B C A' B' C', ~Col A B C -> Par_strict A B A' B' -> Par_strict A C A' C' -> (Par_strict B C B' C' /\ Par A A' B B') -> (Par C C' A A' /\ Par C C' B B').
proof: Proof. intros. spliter. assert(Par C C' A A'). apply par_distincts in H3. spliter. assert(HH:= parallel_existence1 B B' C H5). ex_and HH P. induction(par_dec C P B C). induction H7. apply False_ind. apply H7. exists C. split; Col. spliter. assert(Col P B' C). induction H6. apply False_ind. apply H6. exists B. split; Col. spliter. Col. assert(Col C B B'). apply (col_transitivity_1 _ P); Col. apply False_ind. apply H2. exists B'. split; Col. assert(~ Par C P B' C'). intro. apply H7. apply(par_trans _ _ B' C'); Par. assert(Coplanar C P B' C'). apply coplanar_perm_2, coplanar_trans_1 with B; [|Cop..]. apply not_col_permutation_1, par_not_col with B' C'; Par; Col. assert(HH:=cop_npar__inter_exists C P B' C' H9 H8). ex_and HH C''. induction(eq_dec_points B' C''). subst C''. apply False_ind. induction H6. apply H6. exists B'. split; Col. spliter; apply H2. exists B'. split; Col. apply col_permutation_1. apply(col_transitivity_1 _ P); Col. assert(Par C C'' B B' ). apply (par_col_par_2 _ P); Col. intro. subst C''. apply H2. exists C. split; Col. Par. assert(Par B' C'' B C). apply (par_col_par_2 _ C'); Col. left. Par. assert(~ Col A' B' C'). intro. apply H. assert(Par C' A' B C). apply (par_col_par_2 _ B'). apply par_strict_distinct in H1. spliter. auto. Col. apply par_left_comm. left. Par. assert(Par B C A C). apply (par_trans _ _ A' C'); Par. induction H17. apply False_ind. apply H17. exists C. split; Col. spliter; Col. assert(Par A C A' C''). apply(l13_15_par B A C B' A' C''). intro. apply H. Col. apply par_strict_comm. Par. induction H14. Par. spliter. apply False_ind. apply H2. exists B'. split; Col. Par. Par. assert(C' = C''). apply (l6_21 C' A' B' C'); Col. intro. subst C'. apply H15. Col. eapply (col_par_par_col A C A); Col. apply par_right_comm. left. Par. Par. subst C''. apply (par_trans _ _ B B'); Par. split. Par. apply (par_trans _ _ A A'); Par. Qed.
imports: GeoCoq.Tarski_dev.Ch13_5_Pappus_Pascal