lean_workbook_plus_8870

import Mathlib.Analysis.Complex.Basic

theorem lean_workbook_plus_8870 {a b c : ℝ} (ha : a > 0) (hb : b > 0) (hc : c > 0) : (a^2 + a * b + b^2) * (a^5 * b + 5 * a^4 * b^2 + 4 * a^3 * b^3 + 3 * a^4 * b * c + 16 * a^3 * b^2 * c + 13 / 3 * a^2 * b^2 * c^2) + (b^2 + b * c + c^2) * (b^5 * c + 5 * b^4 * c^2 + 4 * b^3 * c^3 + 3 * b^4 * c * a + 16 * b^3 * c^2 * a + 13 / 3 * b^2 * c^2 * a^2) + (c^2 + c * a + a^2) * (c^5 * a + 5 * c^4 * a^2 + 4 * c^3 * a^3 + 3 * c^4 * a * b + 16 * c^3 * a^2 * b + 13 / 3 * c^2 * a^2 * b^2) ≥ 0   :=  by sorry