rw [div_le_div_iff] <;> simp [mul_add] <;> linarith
n✝¹ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
n✝ n : ℕ
⊢ 1 / ↑(n + 2 - 1) ≤ 2 / ↑(n + 2)
no goals