Sharpness in linear_combination

[b-mehta]

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