lean_workbook_plus_4164
ProvedProve:
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_4164 {a b c : ℝ} : a^2 + b^2 + c^2 - (a * b + b * c + c * a) ≥ 3 * (a - b) * (b - c) := by sorrySource
Prove:
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_4164 {a b c : ℝ} : a^2 + b^2 + c^2 - (a * b + b * c + c * a) ≥ 3 * (a - b) * (b - c) := by sorry