lean_workbook_plus_11949

Proved

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

Now, since $b,c \ge 0$ , using AM-GM, we get $\frac {b + c}{2} \ge \sqrt {bc} \rightarrow (b + c)^2 \ge 4bc$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_11949 :
  ∀ b c : ℝ, b ≥ 0 ∧ c ≥ 0 → (b + c)^2 ≥ 4 * b * c   :=  by sorry

Source