proposition: Lemma l7_21 : forall A B C D P, ~ Col A B C -> B<>D -> Cong A B C D -> Cong B C D A -> Col A P C -> Col B P D -> Midpoint P A C /\ Midpoint P B D.
proof: Proof. intros. assert_diffs. assert (exists P', Cong_3 B D P D B P'). eapply l4_14. Col. Cong. induction H9. assert (Col D B x) by (apply l4_13 with B D P;Col). assert (FSC B D P A D B x C). unfold FSC. unfold Cong_3 in *. spliter. repeat split; Cong; Col. assert (FSC B D P C D B x A). unfold FSC. unfold Cong_3 in *. spliter. repeat split; Col; Cong. assert (Cong P A x C) by (eauto using l4_16). assert (Cong P C x A) by (eauto using l4_16). assert (Cong_3 A P C C x A) by (unfold Cong_3;repeat split; Cong). assert (Col C x A) by (eauto using l4_13). assert (P=x). unfold FSC in *. spliter. apply (l6_21 A C B D); Col. subst x. unfold Cong_3 in *;spliter. split;apply l7_20_bis;Col;Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch06_out_lines GeoCoq.Tarski_dev.Tactics.ColR