lean_workbook_plus_68905
Provedby Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)
WLOG , assume that a≥b≥c>0 . Then we have : \n\n i) b2+c2a2≥c2+a2b2≥a2+b2c2 \n\n ii) 2a+b+cb+c≤2b+c+ac+a≤2c+a+ba+b
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_68905 (a b c : ℝ) (h : a >= b ∧ b >= c ∧ c > 0) :
a^2 / (b^2 + c^2) >= b^2 / (c^2 + a^2) ∧ b^2 / (c^2 + a^2) >= c^2 / (a^2 + b^2) := by sorry
View graph