lean_workbook_plus_4286
ProvedProve that for
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_4286 (k : ℕ) (h : 1 ≤ k) : (1:ℝ) / Real.sqrt (k ^ 2 + k) > (1:ℝ) / (2 * k) := by sorry
Source
Prove that for
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_4286 (k : ℕ) (h : 1 ≤ k) : (1:ℝ) / Real.sqrt (k ^ 2 + k) > (1:ℝ) / (2 * k) := by sorry