lean_workbook_plus_73342
Proved(x+y)(y+z)(z+t)(t+x) \geq (x+y+z+t)(xyz+yzt+ztx+txy), where
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_73342 {x y z t : ℝ} (hx : 0 < x) (hy : 0 < y) (hz : 0 < z) (ht : 0 < t) : (x + y) * (y + z) * (z + t) * (t + x) ≥ (x + y + z + t) * (x * y * z + y * z * t + z * t * x + t * x * y) := by sorrySource