no goals
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B✝ C : Finset α
hA : Finset.Nonempty A
B : Finset α
n : ℕ
⊢ ↑(card (B ^ n)) ≤ (↑(card (A / B)) / ↑(card A)) ^ n * ↑(card A)
simpa only [_root_.pow_zero, div_one] using card_pow_div_pow_le' hA _ _ 0