Prove2Me

lean_workbook_plus_36683

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Using the same substitution as above. We have 0<z≤y≤x0 < z \leq y \leq x , and\n\n∑cyc(s−a)c−ba=∑cycxy−zy+z=(x−y)(x−z)(y−z)(x+y+z)(x+y)(x+z)(y+z)\sum_{\mathrm{cyc}}(s-a)\frac{c-b}{a} = \sum_{\mathrm{cyc}}x\frac{y-z}{y+z} = \frac{(x-y)(x-z)(y-z)(x+y+z)}{(x+y)(x+z)(y+z)}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_36683 :
  ∀ x y z : ℝ,
    0 < x ∧ 0 < y ∧ 0 < z →
    x ≤ y ∧ y ≤ z ∧ z ≤ x →
    0 ≤ (x - y) * (x - z) * (y - z) * (x + y + z) / (x + y) / (x + z) / (y + z)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph