proposition: Lemma l13_15 : forall A B C A' B' C' O , ~Col A B C -> Coplanar 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 O B A C). apply (l13_15_2 A B C A' B' C' O); Col; Par. apply (l13_15_1 A B C A' B' C' O); Col; Par. Qed.
imports: GeoCoq.Tarski_dev.Ch13_5_Pappus_Pascal