lean_workbook_plus_59482
ProvedDerive the final inequality using AM-GM: .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_59482 {x y : ℝ} : 25 * x ^ 2 + 25 * y ^ 2 ≥ 50 * x * y := by sorrySource
Derive the final inequality using AM-GM: .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_59482 {x y : ℝ} : 25 * x ^ 2 + 25 * y ^ 2 ≥ 50 * x * y := by sorry