cases n with
| zero => simp at hs; rw [hs] at hx; contradiction
| succ n => apply Nat.pow_factorization_choose_le; simp
case h
n : ℕ
s : Finset ℕ
hs : n = 0 → s = ∅
x : ℕ
hx : x ∈ s
⊢ x ^ ↑(Nat.factorization (Nat.centralBinom n)) x ≤ 2 * n
no goals