have : ∀ {x y z : ℕ}, x * (2*n) * y * z = (2*n) * (x * y * z) := by intro x y z; linarith
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
n : ℕ
hn : 2 < n
this : ∀ {x y z : ℕ}, x * (2 * n) * y * z = 2 * n * (x * y * z)
⊢ 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