linear_combination for inequalities

[PatrickMassot]

Currently linear_combination cannot be used for inequalities, it would be nice to fix this. Test case would include:

example (x y : ℝ) (h : x < y) : 0 < y - x := by linear_combination h
example (ε : ℝ) (h : 0 < ε) : 0 < ε / 2 := by linear_combination h / 2

example (x y : ℝ) : 0 ≤ x ^ 2 + x * y + y ^ 2 := by
  have h₁ : 0 ≤ (x - y) ^ 2 := by positivity
  have h₂ : 0 ≤ (x + y) ^ 2 := by positivity
  linear_combination h₁ / 4 + 3 * h₂ / 4

And there are extra credit if it can do

example (a b x : ℝ) (h : a ≤ b) : x ^ 2 * a ≤ x ^ 2 * b := by linear_combination x ^ 2 * h

calling positivity to ensure the x^2 coefficient is non-negative.

Somehow there should already be relevant code in the linarith frontend.

[hrmacbeth]

cc @robertylewis who has thought a lot about this.