apply Nat.pow_factorization_choose_le
case h.succ
s : Finset ℕ
x : ℕ
hx : x ∈ s
n : ℕ
hs : Nat.succ n = 0 → s = ∅
⊢ x ^ ↑(Nat.factorization (Nat.centralBinom (Nat.succ n))) x ≤ 2 * Nat.succ n
case h.succ.hn
s : Finset ℕ
x : ℕ
hx : x ∈ s
n : ℕ
hs : Nat.succ n = 0 → s = ∅
⊢ 0 < 2 * Nat.succ n