lean_workbook_plus_76741

Proved

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

Let $a,b\geq 0$ and $2a+ b\leq 3.$ Prove that\n $-3\leq a-b+ab \leq \frac{3}{2}$ \n $-6\leq a-2b+3ab\leq \frac{13}{6}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_76741 (a b : ℝ) (h₁ : 0 ≤ a) (h₂ : 0 ≤ b) (h₃ : 2 * a + b ≤ 3) : -3 ≤ a - b + a * b ∧ a - b + a * b ≤ 3 / 2   :=  by sorry

Source