field_simp positivity discharger with strict neg. hypothesis

Stream: mathlib4

[Li Xuanji]

Comparing these two proofs

import Lean
import Mathlib.Tactic
import Mathlib.Algebra.GroupPower.Order
import Mathlib.Tactic.Positivity

example (c ε: ℝ) (hc : 0 < c) : c * (ε / c) = ε := by {
  field_simp
  ring
}

-- would be nice for this to be `field_simp; ring` too
example (c ε: ℝ) (hc : c < 0) : -c * (ε / -c) = ε := by {
  field_simp [show c ≠ 0 by exact LT.lt.ne hc]
  ring
}

the problem seems to be that positivity proves 0 < c → c ≠ 0 in the first case but it doesn't prove c < 0 → c ≠ 0 in the second