∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : DecidableEq G] {H : AddSubgroup G}
  [inst_2 : DecidablePred fun x => x ∈ H] [inst_3 : H.Normal] {A : Finset G} {m n : ℕ},
  (Finset.image (⇑(QuotientAddGroup.mk' H)) (m • A)).card * {x ∈ n • A | x ∈ H}.card ≤ ((m + n) • A).card