rw [Nat.one_add, Nat.pow_succ]
n : ℕ
hn : 2 < n
⊢ 2 * n * Nat.centralBinom n ≤
    (2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3) * ∏ p in primes (Finset.Ioc n (2 * n)), p
n : ℕ
hn : 2 < n
⊢ 2 * n * Nat.centralBinom n ≤
    (2 * n) ^ Nat.sqrt (2 * n) * (2 * n) * 4 ^ Nat.pred (2 * n / 3) * ∏ p in primes (Finset.Ioc n (2 * n)), p