lean_workbook_plus_1665

Proved

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

Find the maximum value of $ac+bc-c^{2}-ab$ given $a-b=4$ where $a, b, c$ are real numbers.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_1665 (a b c : ℝ) (h : a - b = 4) : a * c + b * c - c ^ 2 - a * b ≤ 4   :=  by sorry

Source