proposition: Lemma l12_18_a : 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.
proof: Proof. intros. assert(Midpoint P A C /\ Midpoint P B D) by (apply l7_21; assumption). spliter. eapply l12_17. intro. subst B. apply H1. apply col_trivial_1. apply H5. apply H6. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles