Make `inv` and `oinv` work with numbers

inversion 1 works but inv 1 does not, which is a shame.

Thanks to Ike we now know how to define a tactic that works on hypotheses as numbers, but unfortunately defining inv 1 s not trivial -- inversion 1 will introduce the to-be-inverted term under some fresh name, which inv should clear, but I haven't found a way to tell inversion which name to use. @robbertkrebbers do you know if that is possible?

The alternative is to re-implement the logic that makes inversion N work, probably as something like "introduce N-1 terms, then introduce the next term under some chosen name, then revert all the other terms". But ideally we don't have to re-implement logic from core Coq tactics...