rwa [sqrt_mul, ← div_div, div_le_iff, div_eq_mul_one_div, ← le_div_iff', one_div (sqrt π)]
n : ℕ
this✝ : 0 < π
this : (Real.sqrt π)⁻¹ ≤ centralBinomialUpper n
⊢ 4 ^ n / Real.sqrt (π * (↑n + 1 / 3)) ≤ ↑(centralBinom n)
n : ℕ
this✝ : 0 < π
this : (Real.sqrt π)⁻¹ ≤ centralBinomialUpper n
⊢ 0 < 4 ^ n

n : ℕ
this✝ : 0 < π
this : (Real.sqrt π)⁻¹ ≤ centralBinomialUpper n
⊢ 0 < Real.sqrt (↑n + 1 / 3)

case hx
n : ℕ
this✝ : 0 < π
this : (Real.sqrt π)⁻¹ ≤ centralBinomialUpper n
⊢ 0 ≤ π