rw [← Real.sqrt_div]
n : ℕ
⊢ (↑n + 1 / 2) / (↑n + 1) ≤ Real.sqrt (↑n + 1 / 3) / Real.sqrt (↑n + 1 + 1 / 3)
n : ℕ
⊢ (↑n + 1 / 2) / (↑n + 1) ≤ Real.sqrt ((↑n + 1 / 3) / (↑n + 1 + 1 / 3))

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