proposition: Lemma l7_13 : forall A P Q P' Q', Midpoint A P' P -> Midpoint A Q' Q -> Cong P Q P' Q'.
proof: Proof. unfold Midpoint. intros. spliter. induction (eq_dec_points P A). treat_equalities;Cong. prolong P' P X Q A. prolong X P' X' Q A. prolong Q' Q Y P A. prolong Y Q' Y' P A. assert (Bet Y A Q') by eBetween. assert (Bet P' A X) by eBetween. assert (Bet A P X) by eBetween. assert(Bet Y Q A) by eBetween. assert (Bet A Q' Y') by eBetween. assert (Bet X' P' A) by eBetween. assert(Bet X A X') by eBetween. assert(Bet Y A Y') by eBetween. assert (Cong A X Y A) by (apply l2_11 with P Q; Cong). assert (Cong A Y' X' A). apply l2_11 with Q' P'; Between. apply cong_transitivity with A Q; Cong. apply cong_transitivity with A P; Cong. assert (Cong A Y A Y'). apply (l2_11 A Q Y _ Q' Y'); Between; Cong. apply cong_transitivity with A P; Cong. assert (Cong X A Y' A) by (apply cong_transitivity with A Y; Cong). assert (Cong A X' A Y) by (apply cong_transitivity with A Y'; Cong). assert (FSC X A X' Y' Y' A Y X). unfold FSC;repeat split; Cong. apply bet_col;auto. eapply (l2_11 X A X' Y' A Y);Between. assert (A <> X). eapply bet_neq12__neq. apply H14. auto. assert (Cong X' Y' Y X) by eauto using l4_16. assert (Cong A X A X') by (apply cong_transitivity with A Y; Cong). assert (IFSC Y Q A X Y' Q' A X') by (unfold IFSC, FSC in *;spliter;repeat split;Between; Cong). assert (Cong Q X Q' X') by eauto using l4_2. assert (IFSC X P A Q X' P' A Q') by (unfold IFSC;repeat split;Between;Cong). eauto using l4_2. Qed.
imports: GeoCoq.Tarski_dev.Ch06_out_lines GeoCoq.Tarski_dev.Tactics.ColR