A quartic inequality in two variables

Expanding and simplifying we get:

$(yz-2y-2z)^2\geq 2yz(2-y-z)\iff y^2z^2 +4y^2+4z^2 \geq 4yz +2y^z+2yz^2$

Now by AM-GM:

${\frac{y^2z^2}{2}+2y^2} \geq 2\sqrt{y^4z^2}=2y^2z$

Similarly $\frac{y^2z^2}{2} +2z^2 \geq 2yz^2$ Also, $2y^2+2z^2\geq 4yz$ by sums of squares Summing the three inequalities yields the result

Source: InternLM Lean-Workbook, record lean_workbook_3247 (Apache-2.0). The complete source proposition and explicit variable declarations are preserved.