apply Nat.pow_factorization_choose_le
case h
n : ℕ
s : Finset ℕ
hn : 0 < n
x : ℕ
a✝ : x ∈ s
⊢ x ^ ↑(Nat.factorization (Nat.centralBinom n)) x ≤ 2 * n
case h.hn
n : ℕ
s : Finset ℕ
hn : 0 < n
x : ℕ
a✝ : x ∈ s
⊢ 0 < 2 * n