lean_workbook_plus_29710

Proved

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

Either $\sqrt{b^2-4ac}\le |b|-2$ and so $|b|\ge 2$ and $-4ac\le -4|b|+4$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_29710 (a b c : ℝ) (h : 0 < a) (h2 : 0 < c) : (Real.sqrt (b ^ 2 - 4 * a * c) ≤ |b| - 2 → |b| ≥ 2 ∧ -4 * a * c ≤ -4 * |b| + 4)   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph