lean_workbook_plus_80900

Proved

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

Let $a\ge b\ge c\ge d$ be real numbers such that $a+b+c+d=2$ . Prove that $a^2+2bc+d^2\ge 1.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

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

Source