lean_workbook_plus_42389
ProvedProve that
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_42389 (a : ℝ) : (a - 1) * (3 * a - 7) ≥ 4 * |a - 5 / 3| - 8 / 3 := by sorry
Source
Prove that
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_42389 (a : ℝ) : (a - 1) * (3 * a - 7) ≥ 4 * |a - 5 / 3| - 8 / 3 := by sorry