Prove2Me

lean_workbook_plus_34773

Proved

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

⇔a(a+b)(a+c)≥(a+b)bc+(a+c)bc⇔(a2−bc)(a+b+c)≥0 \Leftrightarrow a(a+b)(a+c)\geq (a+b)bc+(a+c)bc \Leftrightarrow (a^2-bc)(a+b+c)\geq 0

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_34773 (a b c : ℝ) : a * (a + b) * (a + c) ≥ (a + b) * b * c + (a + c) * b * c ↔ (a^2 - b * c) * (a + b + c) ≥ 0   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph