lean_workbook_plus_37377

Open

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Prove that $(e^y+e^{-y})^2 \ge (e^y-e^{-y})^2$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_37377 : ∀ y : ℝ, (exp y + exp (-y)) ^ 2 ≥ (exp y - exp (-y)) ^ 2   :=  by sorry

Source