lean_workbook_plus_1964
Provedprove that $\frac {a+t}{x+t}+\frac {b+t}{y+t}+\frac {c+t}{z+t}\leq \frac {a}{x}+\frac {b}{y}+\frac {c}{z}$ given $x,y,z,a,b,c>0$ and $a \geq x,b \geq y,c \geq z, t \geq 0$
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_1964 (x y z a b c t : ℝ) (hx : 0 < x) (hy : 0 < y) (hz : 0 < z) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) (hab : a ≥ x) (hbc : b ≥ y) (hca : c ≥ z) (h : t ≥ 0) : (a + t) / (x + t) + (b + t) / (y + t) + (c + t) / (z + t) ≤ a / x + b / y + c / z := by sorry
Source