A rational bound from a linear constraint

Let $x=\sum_{cyc}a^2$ and $y=\sum_{cyc}ab,$ so that we have $x+2y=9$ and $x\ge y,$ leading to $\frac{(x+y)^2}{2(x+y)+27}=\frac{x+y}{2+\frac{27}{x+y}}\geq \frac{2(x+y)}{13}$

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