proposition: Lemma l12_18 : forall A B C D P, Cong A B C D -> Cong B C D A -> ~Col A B C -> B <> D -> Col A P C -> Col B P D -> Par A B C D /\ Par B C D A /\ TS B D A C /\ TS A C B D.
proof: Proof. intros. split. apply (l12_18_a _ _ _ _ P); assumption. split. apply (l12_18_b _ _ _ _ P); assumption. split. apply (l12_18_c _ _ _ _ P); assumption. apply (l12_18_d _ _ _ _ P); assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles