Prove that for x,y,z>0, F=(3\*y2+3\*z2−4\*y\*z)\*x5+(y+z)\*(16\*z2−21\*y\*z+16\*y2)\*x4+(−38\*y2\*z2+18\*y3\*z+27\*y4+27\*z4+18\*y\*z3)\*x3+(y+z)\*(19\*z4+3\*y\*z3−70\*y2\*z2+3\*y3\*z+19\*y4)\*x2+(10\*y5\*z−41\*y2\*z4+10\*y\*z5+6\*y6−100\*y3\*z3−41\*y4\*z2+6\*z6)\*x+(y+z)\*(z2+y\*z+y2)\*(z4+5\*y\*z3+9\*y2\*z2+5\*y3\*z+y4)≥0
Source: InternLM Lean-Workbook, record lean_workbook_plus_9349 (Apache-2.0). Complete source proposition preserved; proof developed independently.
Preamble
import Mathlib
open Real Nat
Formal statement
theorem WorkbookSource.plus_9349 (x y z : ℝ) (hx : 0 < x) (hy : 0 < y) (hz : 0 < z) : (3 * y ^ 2 + 3 * z ^ 2 - 4 * y * z) * x ^ 5 + (y + z) * (16 * z ^ 2 - 21 * y * z + 16 * y ^ 2) * x ^ 4 + (-38 * y ^ 2 * z ^ 2 + 18 * y ^ 3 * z + 27 * y ^ 4 + 27 * z ^ 4 + 18 * y * z ^ 3) * x ^ 3 + (y + z) * (19 * z ^ 4 + 3 * y * z ^ 3 - 70 * y ^ 2 * z ^ 2 + 3 * y ^ 3 * z + 19 * y ^ 4) * x ^ 2 + (10 * y ^ 5 * z - 41 * y ^ 2 * z ^ 4 + 10 * y * z ^ 5 + 6 * y ^ 6 - 100 * y ^ 3 * z ^ 3 - 41 * y ^ 4 * z ^ 2 + 6 * z ^ 6) * x + (y + z) * (z ^ 2 + y * z + y ^ 2) * (z ^ 4 + 5 * y * z ^ 3 + 9 * y ^ 2 * z ^ 2 + 5 * y ^ 3 * z + y ^ 4) ≥ 0 := by sorry