A degree-eight bound involving pairwise squared sums

substitute $a=\frac{x}{x+y+z}$ etc.[x,y,z>0] then it turns into $\frac{(x^2+y^2)(y^2+z^2)(z^2+x^2)}{(x+y+z)^6} \ge 8\frac{(x^2y^2+y^2z^2+z^2x^2)^2}{(x+y+z)^8}$

i.e. $(x+y+z)^2(x^2+y^2)(z^2+x^2)(y^2+z^2) \ge 8(x^2y^2+y^2z^2+z^2x^2)^2$

now it is a symmetric inequality in x,y,z , which can be proved using murihead inequality

Source: InternLM Lean-Workbook, record lean_workbook_2054 (Apache-2.0). Complete source proposition preserved; proof developed independently.