lean_workbook_plus_74732
DisprovedPreamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_74732 : ∀ x y : ℝ, (x / (y + 3) + 2 * y / (x + 1) ≥ 1 / 5 ↔ 4 * x ^ 2 - 12 * x + 9 ≥ 0) := by sorry
Source
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_74732 : ∀ x y : ℝ, (x / (y + 3) + 2 * y / (x + 1) ≥ 1 / 5 ↔ 4 * x ^ 2 - 12 * x + 9 ≥ 0) := by sorry