lean_workbook_plus_62980
ProvedGiven that and , show that
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_62980 (a b c : ℝ) (h : (a + 1) * (b + 1) * (c + 1) = 8) (ha : a ≥ 0) (hb : b ≥ 0) (hc : c ≥ 0) : a * b * c ≤ 1 := by sorry
Source