Lean-Workbook Plus 37377: Exponential inequality

For every real $y$, $(e^y+e^{-y})^2\ge(e^y-e^{-y})^2$.

Source: Lean-Workbook row lean_workbook_plus_37377 (Apache-2.0). The unchanged proposition comes from the original record; its missing mathematical imports and namespaces are restored here.