proposition: Lemma cong_mid2__cong : forall A M B A' M' B', Midpoint M A B -> Midpoint M' A' B' -> Cong A M A' M' -> Cong A B A' B'.
proof: Proof. intros A M B A' M' B' HM HM' HCong. destruct HM. destruct HM'. apply (l2_11 _ M _ _ M'); auto. apply (cong_transitivity _ _ A' M'); auto. apply (cong_transitivity _ _ A M); Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch06_out_lines GeoCoq.Tarski_dev.Tactics.ColR