∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : CommGroup G] {A B C : Finset G},
  A.Nonempty →
    A ⊆ B →
      (∀ A' ∈ B.powerset.erase ∅, ↑(A * C).card / ↑A.card ≤ ↑(A' * C).card / ↑A'.card) →
        ∀ A' ⊆ A, (A * C).card * A'.card ≤ (A' * C).card * A.card