rw [div_pow, div_le_div_iff]
n : ℕ
⊢ ((↑n + 1 / 2) / (↑n + 1)) ^ 2 ≤ (↑n + 1 / 3) / (↑n + 1 + 1 / 3)

case hx
n : ℕ
⊢ 0 ≤ ↑n + 1 / 3
n : ℕ
⊢ (↑n + 1 / 2) ^ 2 * (↑n + 1 + 1 / 3) ≤ (↑n + 1 / 3) * (↑n + 1) ^ 2

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

case d0
n : ℕ
⊢ 0 < ↑n + 1 + 1 / 3

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