lean_workbook_plus_55013

import Mathlib.Analysis.Complex.Basic

theorem lean_workbook_plus_55013 : ∀ p : ℝ, (p - 1) ^ 2 * (4 * p ^ 3 + 6 * p ^ 2 + 9 * p + 8) * (2 * p ^ 4 + 10 * p ^ 3 + 9 * p ^ 2 + 16 * p + 8) ≥ 0   :=  by sorry