A cubic bound on an interval

Let $u=a+b+c,v=ab+bc+ca,w=abc$ . By Schur we get $w\ge \frac{4uv-u^3}{9}=\frac{4v-9}{3}$ While $x=\sqrt{\frac{a^2+b^2+c^2}{3}}=\sqrt{\frac{9-2v}{3}}\Longleftrightarrow v=\frac{9-3x^2}{2}$ So we just need to prove $3-2x^2\ge \frac{x}{2}\cdot ( 3x^2-16x+15)\Longleftrightarrow (x-2)(x-1)^2\le 0$

Source: InternLM Lean-Workbook, record lean_workbook_45345; Apache-2.0. Complete source proposition preserved.