Mathlib linear_combination on ≤: coefficients must be provably nonnegative

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.