Reserve more notation in `integers.v`.

Avoid duplicating details like at level 35.

This is a bit of a slippery slope. (I reserved just the notation that I overload elsewhere.)