lean_workbook_plus_16360

Proved

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

Using the condition $a \leq b + c$ and $a, b, c \leq 1$ , prove the inequality $(1-a)(1-b)(1-c) \geq 0$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_16360 (a b c : ℝ) (h₁ : a ≤ b + c) (h₂ : a ≤ 1 ∧ b ≤ 1 ∧ c ≤ 1) :
  (1 - a) * (1 - b) * (1 - c) ≥ 0   :=  by sorry

Source