proposition: Lemma l8_20_1 : forall A B C C' D P, Per A B C -> Midpoint P C' D -> Midpoint A C' C -> Midpoint B D C -> Per B A P.
proof: Proof. intros. double B A B'. double D A D'. double P A P'. induction (eq_dec_points A B). subst B. unfold Midpoint in H5. spliter. eapply l8_2. eapply l8_5. assert (Per B' B C). eapply l8_3. apply H. assumption. unfold Col. left. apply midpoint_bet. assumption. assert (Per B B' C'). eapply l8_10. apply H7. unfold Cong_3. repeat split. apply cong_pseudo_reflexivity. eapply l7_13. unfold Midpoint. split. apply H3. apply midpoint_cong. assumption. assumption. eapply l7_13. apply l7_2. apply H3. assumption. assert(Midpoint B' D' C'). eapply symmetry_preserves_midpoint. apply H4. apply H3. apply l7_2. apply H1. assumption. assert(Midpoint P' C D'). eapply symmetry_preserves_midpoint. apply H1. apply H5. apply H4. assumption. unfold Per. exists P'. split. assumption. unfold Per in H7. ex_and H7 D''. assert (D''= D). eapply symmetric_point_uniqueness. apply H7. apply l7_2. assumption. subst D''. unfold Per in H8. ex_and H8 D''. assert (D' = D''). eapply symmetric_point_uniqueness. apply l7_2. apply H9. assumption. subst D''. assert (Midpoint P C' D). eapply symmetry_preserves_midpoint. apply l7_2. apply H1. apply l7_2. apply H5. apply l7_2. apply H4. assumption. assert (Cong C D C' D'). eapply l7_13. apply H1. apply l7_2. assumption. assert (Cong C' D C D'). eapply l7_13. apply l7_2. apply H1. apply l7_2. assumption. assert(Cong P D P' D'). eapply l7_13. apply l7_2. apply H5. apply l7_2. assumption. assert (Cong P D P' C). eapply cong_transitivity. apply H16. unfold Midpoint in H10. spliter. apply cong_right_commutativity. apply cong_symmetry. assumption. assert (IFSC C' P D B D' P' C B). unfold IFSC. repeat split. apply midpoint_bet. assumption. apply midpoint_bet. apply l7_2. assumption. apply cong_right_commutativity. assumption. assumption. apply cong_commutativity. assumption. apply cong_right_commutativity. apply midpoint_cong. assumption. assert (Cong P B P' B). eapply l4_2. apply H18. apply cong_commutativity. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR