lean_workbook_plus_71539
ProvedBut
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_71539 (a b : ℝ) (hab : a + b > 2) : (a + b) ^ 2 / (a + b - 2) ≥ 8 ↔ (a + b - 4) ^ 2 ≥ 0 := by sorry
Source
But
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_71539 (a b : ℝ) (hab : a + b > 2) : (a + b) ^ 2 / (a + b - 2) ≥ 8 ↔ (a + b - 4) ^ 2 ≥ 0 := by sorry