lean_workbook_plus_78314

Proved

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

Derive the inequality $\frac{a^2}{b^2} + 1 \le \frac{5a}{2b}$ from $\left( \frac{a}{b} - \frac{1}{2} \right) \left( \frac{a}{b} -2 \right) \le 0$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_78314 (a b : ℝ) (hab : b ≠ 0) (h : (a / b - 1 / 2) * (a / b - 2) ≤ 0) :
  a^2 / b^2 + 1 ≤ 5 * a / (2 * b)   :=  by sorry

Source