proposition: Lemma l13_18 : 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') /\ ((Par_strict B C B' C' /\ Par A A' B B') -> (Par C C' A A' /\ Par C C' B B')) /\ (Par A A' B B' /\ Par A A' C C' -> Par B C B' C').
proof: Proof. intros. spliter. split. intros. apply (l13_18_2 A B C A' B' C' O); auto. split. intros. spliter. apply l13_18_3; auto. intros. spliter. apply (l13_15_par A B C A' B' C'); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_5_Pappus_Pascal