Sharpness in linear_combination

It would be nice if there is a flag I can turn on in linear_combination so that it gives me a warning/info message which tells me whether or not there was slack in the inequality at the end?
That is, I think the very last step of the tactic is after we're in the form c <= 0 where c is an explicit numeral, it asks norm_num or something to prove this. I'd like to know whether c = 0 or c < 0 at the end.

The idea is that I'd like it to be easy to figure out which inequalities throughout my proof had some slack in the numerical constants, and which ones didn't. Certainly this shouldn't be the default setting, and I don't really mind if it's a trace option or a setting I need to turn on at each call, whatever's easiest to implement.

A temporary workaround for this, provided by @hrmacbeth, is as follows

import Mathlib

macro "hack" : tactic => do `(tactic | (ring_nf; apply le_refl))

-- works
example {x : ℝ} (hx : x ≤ 3) : x ≤ 3 := by linear_combination (norm := hack) hx

 -- fails, `⊢ -4 ≤ 0`
example {x : ℝ} (hx : x ≤ 3) : x ≤ 7 := by linear_combination (norm := hack) hx

Start with the linear_combination tactic and reproduce the two examples in the issue, including the custom norm workaround. Determine how an opt-in flag or trace option can report whether the final explicit numeral is zero or negative, and verify that the default behavior remains unchanged.