have := centralBinomialLower_monotone.ge_of_tendsto centralBinomialLower_limit n
n : ℕ
this : 0 < π
⊢ ↑(centralBinom n) ≤ 4 ^ n / Real.sqrt (π * (↑n + 1 / 4))
n : ℕ
this✝ : 0 < π
this : centralBinomialLower n ≤ (Real.sqrt π)⁻¹
⊢ ↑(centralBinom n) ≤ 4 ^ n / Real.sqrt (π * (↑n + 1 / 4))