lean_workbook_plus_55045
Disprovedprove that $0\leq \frac {a \left( b+c \right) }{x \left( y+z \right) }+\frac {b \left( c+a \right) }{y \left( z+x \right) }+\frac {c \left( a+b \right) }{z \left( x+y \right) }-\frac {a}{x}-\frac {b}{y}-\frac {c}{z}$ given $a \geq x,b \geq y,c \geq z$
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_55045 : ∀ a b c x y z : ℝ, a ≥ x ∧ b ≥ y ∧ c ≥ z → 0 ≤ a * (b + c) / (x * (y + z)) + b * (c + a) / (y * (z + x)) + c * (a + b) / (z * (x + y)) - a / x - b / y - c / z := by sorry
Source