lean_workbook_plus_47693

Proved

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

Prove that $\frac{3a^2-1}{(3-2a^2)(a^2+2)}\geq\frac{27a^2-9}{49}$ for $a^2 \leq 1$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_47693 (a : ℝ) (ha : a^2 ≤ 1) : (3 * a^2 - 1) / ((3 - 2 * a^2) * (a^2 + 2)) ≥ (27 * a^2 - 9) / 49   :=  by sorry

Source