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