rw [← Nat.prod_pow_factorization_centralBinom]
case h
n : ℕ
hn : 2 < n
⊢ Nat.centralBinom n ≤ (2 * n) ^ Nat.sqrt (2 * n) * 4 ^ Nat.pred (2 * n / 3) * ∏ p in primes (Finset.Ioc n (2 * n)), p
case h
n : ℕ
hn : 2 < n
⊢ ∏ p in Finset.range (2 * n + 1), p ^ ↑(Nat.factorization (Nat.centralBinom n)) p ≤
    (2 * n) ^ Nat.sqrt (2 * n) * 4 ^ Nat.pred (2 * n / 3) * ∏ p in primes (Finset.Ioc n (2 * n)), p