lean_workbook_plus_40320

Proved

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

Let $a, b\geq 1$ and $a+\frac{1}{a^2} \geq b-\frac{2}{b^2}.$ Show that

a\geq \frac{b}{2}-\frac{1}{b^2}

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_40320 (a b : ℝ) (hab : 1 ≤ a ∧ 1 ≤ b) (h : a + 1 / a ^ 2 ≥ b - 2 / b ^ 2) : a ≥ b / 2 - 1 / b ^ 2   :=  by sorry

Source