apply Nat.mul_le_mul_left
n : ℕ
hn : 2 < n
⊢ 2 * n * Nat.centralBinom n ≤
    2 * 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
⊢ Nat.centralBinom n ≤ (2 * n) ^ Nat.sqrt (2 * n) * 4 ^ Nat.pred (2 * n / 3) * ∏ p in primes (Finset.Ioc n (2 * n)), p