An eighth-degree cyclic inequality for nonnegative variables

Prove that for $x,y,z\geq 0$, $-xyz(x^2y^3+y^2z^3+x^3z^2)+1/3(x^2y^2+y^2z^2+x^2z^2)^2\geq 0$

Source: InternLM Lean-Workbook, record lean_workbook_6994 (Apache-2.0). Natural-language proposition preserved; raw Lean transcription corrected: Restore the nonnegative domain assumptions for x, y, z explicitly stated in the natural-language source and omitted by the raw Lean transcription. Proof developed independently.