lean_workbook_plus_7867

Proved

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

Let $x_i>x_j$ , then ${x_ix_j(x_i-x_j)<\frac{x_i^2+x_ix_j+x_j^2}{3}(x_i-x_j}=\frac{x_i^3-x_j^3}{3}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_7867 (x_i x_j : ℝ) (h : x_i > x_j) :
  x_i * x_j * (x_i - x_j) < (x_i ^ 2 + x_i * x_j + x_j ^ 2) * (x_i - x_j)   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph