lean_workbook_plus_20066

Proved

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

Either $|b|\ge 2$ and $ac+1\ge |b|$ , which implies $(ac+1)^2\ge b^2$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_20066  (a b c : ℝ)
  (h₀ : abs b ≥ 2)
  (h₁ : a * c + 1 ≥ abs b) :
  (a * c + 1)^2 ≥ b^2   :=  by sorry

Source