lean_workbook_plus_2281
ProvedProve that if , then .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_2281 (a b : ℝ) (h₁ : b ≥ a) : b^3 - 12*b + 16 ≥ a^3 - 12*a - 16 := by sorry
Source
Prove that if , then .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_2281 (a b : ℝ) (h₁ : b ≥ a) : b^3 - 12*b + 16 ≥ a^3 - 12*a - 16 := by sorry