proposition: Lemma l12_18_d : 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 -> TS A C B D.
proof: Proof. intros. assert(Midpoint P A C /\ Midpoint P B D) by (apply l7_21; assumption). eapply (l12_18_c _ _ _ _ P). Cong. Cong. intro. apply H1. assert(Col A B P). eapply col_permutation_2. eapply col_transitivity_1. apply H2. Col. Col. eapply (col_transitivity_1 _ P). intro. subst P. spliter. apply is_midpoint_id in H5. subst C. contradiction. Col. Col. intro. subst C. apply H1. apply col_trivial_3. Col. Col. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles