lean_workbook_plus_34371
ProvedPreamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_34371 : ∀ a b : ℝ, Real.sqrt (a ^ 2 - a * b + b ^ 2) ≥ (a + b) / 2 ↔ (a - b) ^ 2 ≥ 0 := by sorry
Source
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_34371 : ∀ a b : ℝ, Real.sqrt (a ^ 2 - a * b + b ^ 2) ≥ (a + b) / 2 ↔ (a - b) ^ 2 ≥ 0 := by sorry