∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : Group G] {A : Finset G} {K : ℝ} {m : ℕ},
  3 ≤ m →
    ↑(A ^ 3).card ≤ K * ↑A.card →
      ∀ (ε : Fin m → ℤ),
        (∀ (i : Fin m), |ε i| = 1) →
          ↑(List.map (fun i => A ^ ε i) (List.finRange m)).prod.card ≤ K ^ (3 * (m - 2)) * ↑A.card