lean_workbook_plus_56059
Provedby Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)
Firstly, we have the inequality: x+1x≥x4+3x⇔x4+3≥(x+1)2⇔(x−1)2(x2+2x+2)≥0 ( which is obvious )
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_56059 (x : NNReal) :
x / (x + 1) ≥ x / (Real.sqrt (x^4 + 3)) := by sorry
View graph