lean_workbook_plus_33907
DisprovedPreamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_33907 : ∀ c : ℝ, (4 / 3 + (4 * c * (2 - c) * (c - 1) ^ 2) / ((c ^ 2 + 2) * ((2 - c) ^ 2 + 2))) ≥ 4 / 3 := by sorry
Source
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_33907 : ∀ c : ℝ, (4 / 3 + (4 * c * (2 - c) * (c - 1) ^ 2) / ((c ^ 2 + 2) * ((2 - c) ^ 2 + 2))) ≥ 4 / 3 := by sorry