Prove2Me

lean_workbook_plus_42857

Proved

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

ObservationYou could use the observation that: \n\nFor any x∈R+x \in \mathbb{R^+} : \n\n x5−x2+3≥x3+2⇒x^5 - x^2 + 3 \geq x^3 + 2 \Rightarrow 1x5−x2+3≤1x3+2\frac{1}{x^5 - x^2 + 3} \leq \frac{1}{x^3 + 2} \n\nhttps://artofproblemsolving.com/community/c6h5383p17397

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_42857  (x : ℝ)
  (h₀ : 0 < x)
  (h₁ : x^5 - x^2 + 3 ≥ x^3 + 2) :
  1 / (x^5 - x^2 + 3) ≤ 1 / (x^3 + 2)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph