lean_workbook_plus_70146
Proved;
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_70146 {a b c : ℝ} :
a ^ 4 * b ^ 2 + a ^ 4 * c ^ 2 + b ^ 4 * c ^ 2 + b ^ 4 * a ^ 2 + c ^ 4 * a ^ 2 + c ^ 4 * b ^ 2 ≥ a ^ 4 * b * c + a ^ 4 * c * b + b ^ 4 * c * a + b ^ 4 * a * c + c ^ 4 * a * b + c ^ 4 * b * a ↔ a ^ 4 * (b - c) ^ 2 + b ^ 4 * (c - a) ^ 2 + c ^ 4 * (a - b) ^ 2 ≥ 0 := by sorrySource