lean_workbook_plus_50534

import Mathlib.Analysis.Complex.Basic

theorem lean_workbook_plus_50534 {a b c : ℝ} : 2 * (a ^ 8 - a ^ 6 * b ^ 2 - a ^ 6 * c ^ 2 + a ^ 4 * b ^ 2 * c ^ 2) + 2 * (b ^ 8 - b ^ 6 * c ^ 2 - b ^ 6 * a ^ 2 + b ^ 4 * c ^ 2 * a ^ 2) + 2 * (c ^ 8 - c ^ 6 * a ^ 2 - c ^ 6 * b ^ 2 + c ^ 4 * a ^ 2 * b ^ 2) ≥ 0   :=  by sorry