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