The integers as normed ring #
This file contains basic facts about the integers as normed ring.
∥n∥ denotes the norm of
n as real number.
This norm is always nonnegative, so we can bundle the norm together with this fact,
to obtain a term of type
nnreal (the nonnegative real numbers).
The resulting nonnegative real number is denoted by