Make `inv` and `oinv` work with numbers

I also replaced all inversion_clear by inv. In list.v I furthermore replaced most inversion by inv just to get a whole lot of extra testcases. However sometimes, follow-up automation fails when the inverted hypothesis is cleared.

Fixes #199 (closed)