let linear_combination solve ≠ goals

[hrmacbeth]

Goals a ≠ b turn up quite often when working over general fields, notably goals a ≠ 0 to allow for the use of field_simp with a denominator a.

Often this can be solved by contrapose! followed by linear_combination. It would be nice to fold the contrapose! into a preprocessing step of linear_combination.

Example:

example {x y z : K} (h₁ : (x - y) ^ 2 ≠ 0) (h₂ : y = z) : -x ^ 2 + 2 * x * z ≠ y ^ 2 :=
begin
  contrapose! h₁,
  linear_combination (h₁, -1) (h₂, - 2 * x),
end

(current mathlib) should become

example {x y z : K} (h₁ : (x - y) ^ 2 ≠ 0) (h₂ : y = z) : -x ^ 2 + 2 * x * z ≠ y ^ 2 :=
by linear_combination (h₁, -1) (h₂, - 2 * x)

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/.60linear_combination.60.20for.20.20.E2.89.A0.20goals