lean_workbook_plus_55382

import Mathlib.Analysis.Complex.Basic

theorem lean_workbook_plus_55382 : ∀ p u : ℝ, (-4 * p^4 + 16 * p^3 + 16 * p^2) * u^2 + (-24 * p^4 + 52 * p^3 + 52 * p^2 + 16) * u + 4 * p^4 - 32 * p^2 + 64 ≥ 0   :=  by sorry