Prove2Me

lean_workbook_plus_76439

Proved

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

WLOG assume (a−1)(b−1)≥0(a-1)(b-1)\ge 0 Thus c(a−1)(b−1)≥0  ⟹  abc≥bc+ca−c  ⟹  2abc≥2bc+2ca−2cc(a-1)(b-1)\ge 0\implies abc\ge bc+ca-c\implies 2abc\ge 2bc+2ca-2c Hence we must prove a2+b2+c2+2bc+2ca−2c+1≥2ab+2bc+2ca  ⟹  (a−b)2+(c−1)2≥0a^2+b^2+c^2+2bc+2ca-2c+1\ge 2ab+2bc+2ca\implies (a-b)^2+(c-1)^2\ge 0 which is obvious

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

View graph