lean_workbook_plus_13017

If we're in the bad case, we can pick new variables $u=\tfrac{1}{x}, v=\tfrac{1}{y}, w=\tfrac{1}{z}$ (in 'good' cyclic order) and substitute into the original proposition to find: $\sum_\text{cyc} \frac{ (v+u)^2 v^2 }{ (v+u)^2 } \le 3$