rw [centralBinomialLower, centralBinomialLower, _root_.pow_succ, ←div_div]
n : ℕ
⊢ centralBinomialLower n ≤ centralBinomialLower (n + 1)
n : ℕ
⊢ ↑(centralBinom n) * Real.sqrt (↑n + 1 / 4) / 4 ^ n ≤
    ↑(centralBinom (n + 1)) * Real.sqrt (↑(n + 1) + 1 / 4) / 4 / 4 ^ n