lean_workbook_plus_52998
Provedprove that for .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_52998 (x : ℝ) (hx : 0 ≤ x) : (1 + x ^ 2) ^ 3 / (1 + x) ^ 3 ≥ (1 + x ^ 3) / 2 := by sorry
Source
prove that for .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_52998 (x : ℝ) (hx : 0 ≤ x) : (1 + x ^ 2) ^ 3 / (1 + x) ^ 3 ≥ (1 + x ^ 3) / 2 := by sorry