Theorem: limit_const_add_inv_succ (LeanTeaching/TutoLib.lean)

State before:
x : ℝ
n : ℕ
⊢ |x + 1 / (↑n + 1) - x| ≤ 1 / (↑n + 1)
Tactic:
rw [abs_of_pos] <;> linarith [@Nat.one_div_pos_of_nat ℝ _ n]
State after:
no goals