Require ZArith.
Check `32`.
Check [f:nat->Z]`(f O) + 0`.