lean_workbook_plus_56565

Proved

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

Prove that $x^5-2x^4-3x^3+12x-8\leq0$ when $3x^3-6x^2+5x-12\leq0$ and $x\geq0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_56565 : ∀ x : ℝ, (x >= 0 ∧ 3 * x ^ 3 - 6 * x ^ 2 + 5 * x - 12 <= 0) → x ^ 5 - 2 * x ^ 4 - 3 * x ^ 3 + 12 * x - 8 <= 0   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph