lean_workbook_plus_9321
ProvedIt was explained in a better post; here it is: .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_9321 (x y : ℝ) : x * (y - x) ≤ (x + (y - x))^2 / 4 := by sorry
Source
It was explained in a better post; here it is: .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_9321 (x y : ℝ) : x * (y - x) ≤ (x + (y - x))^2 / 4 := by sorry