proposition: Lemma l7_16 : forall P Q R S P' Q' R' S' A, Midpoint A P P' -> Midpoint A Q Q' -> Midpoint A R R' -> Midpoint A S S' -> Cong P Q R S -> Cong P' Q' R' S'.
proof: Proof. intros. assert (Cong P Q P' Q'). eapply l7_13. apply l7_2. apply H. apply l7_2. apply H0. assert (Cong R S R' S'). eapply l7_13. apply l7_2. apply H1. apply l7_2. apply H2. apply cong_transitivity with P Q; Cong. apply cong_transitivity with R S; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch06_out_lines GeoCoq.Tarski_dev.Tactics.ColR