Prove2Me

lean_workbook_plus_12389

Proved

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

a2(a3−1)a3+1≥3(a−1)2⟺2a2(a−1)(a2+a+1)a3+1≥3(a−1)\frac{a^{2}(a^{3}-1)}{a^{3}+1} \ge \frac{3(a-1)}{2} \Longleftrightarrow \frac{2a^{2}(a-1)(a^2+a+1)}{a^{3}+1} \ge 3(a-1)

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_12389 : ∀ a : ℝ, a ≠ -1 ∧ a ≠ 1 → a^2 * (a^3 - 1) / (a^3 + 1) ≥ 3 * (a - 1) / 2 ↔ 2 * a^2 * (a - 1) * (a^2 + a + 1) / (a^3 + 1) ≥ 3 * (a - 1)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph