lean_workbook_plus_19412

Proved

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

If $b+c\ge 2\sqrt{10}$ , by Cauchy we have $(b^2+10)(c^2+10)\ge 10(b+c)^2=10(12-a)^2$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_19412  (b c : ℝ)
  (h₀ : 2 * Real.sqrt 10 ≤ b + c) :
  (b^2 + 10) * (c^2 + 10) ≥ 10 * (b + c)^2   :=  by sorry

Source