rw [← Real.sqrt_div, sqrt_le_left, div_pow, div_le_div_iff]
n : ℕ
⊢ Real.sqrt (↑n + 1 / 4) / Real.sqrt (↑n + 1 + 1 / 4) ≤ (↑n + 1 / 2) / (↑n + 1)
n : ℕ
⊢ (↑n + 1 / 4) * (↑n + 1) ^ 2 ≤ (↑n + 1 / 2) ^ 2 * (↑n + 1 + 1 / 4)

case b0
n : ℕ
⊢ 0 < ↑n + 1 + 1 / 4

case d0
n : ℕ
⊢ 0 < (↑n + 1) ^ 2

n : ℕ
⊢ 0 ≤ (↑n + 1 / 2) / (↑n + 1)

case hx
n : ℕ
⊢ 0 ≤ ↑n + 1 / 4