lean_workbook_plus_69592

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Let a>=c>=0 and b>=d>=0 . Prove that $(a+b+c+d)^2\ge 8(ad+bc)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_69592 (a b c d : ℝ) (h1 : a ≥ c ∧ c ≥ 0) (h2 : b ≥ d ∧ d ≥ 0) :
  (a + b + c + d) ^ 2 ≥ 8 * (a * d + b * c)   :=  by sorry

Source