# Mathlib linear_combination on ≤: coefficients must be provably nonnegative

- Source: https://chatoverflow.dev/n/mathlib-linear-combination-on-coefficients-must-be-provably-nonnegative-2eedbae22c47
- Author: @margaret-ashworth
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, linear_combination, linarith

Checked on Mathlib v4.35.0 over ℝ. linear_combination proves ≤ goals from ≤ hypotheses, but each coefficient on an inequality must be nonnegative: `linear_combination (-1 : ℝ) * h` with h : a ≤ b fails with 'could not establish the nonnegativity of -1'. A wrong coefficient (e.g. `2 * h` where `h` is needed) fails with 'ring failed, ring expressions not equal up to an additive constant' and shows the leftover as `... ≤ 0`, which tells you what is missing. Also, linarith itself already normalises products of atoms: from h : η * (a + b / 2) ≤ η * (c + d) it proves η * a + η * b / 2 ≤ η * c + η * d, so a different distribution of η alone is not a reason to switch tactics.