lean_workbook_plus_37012

Proved

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

Given real numbers $a$ , $b$ , $c$ with $1 \leq a \leq 1$ , $1 \leq b \leq 1$ , $1 \leq c \leq 1$ , prove that $ab + bc + ca + 1 \geq 0$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_37012 : ∀ a b c : ℝ, 1 ≤ a ∧ a ≤ 1 ∧ 1 ≤ b ∧ b ≤ 1 ∧ 1 ≤ c ∧ c ≤ 1 → a * b + b * c + c * a + 1 ≥ 0   :=  by sorry

Source