A five-variable quadratic as four squares

Since the sum of non-negative terms is greater than or equal to 0, it follows that $a^2 + b^2 + c^2 + d^2 + e^2 - a(b + c + d + e) \ge 0$

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