Rodin User’s Handbook v.2.8: Arithmetic

2.5.6 Arithmetic

We have the usual operations on integers, $+$ , $-$ , $\cdot$ and $\div$ (ASCII: +, -, * and /). They can be compared with the usual equality operators: $<$ , $\leq$ , $\geq$ , $>$ (ASCII: <, <=, >=, >).

$\mathord {\mathbb Z}$ (ASCII: INT) denotes the set of all integer numbers. $\mathord {\mathbb N}$ and $\mathord {\mathbb N}_1$ (ASCII: NAT and NAT1 respectively) are the subsets of natural numbers.

$\includegraphics[width=7mm]{img/info_64.png}$
If you specify two variables $x$ and $y$ with $x\in \mathord {\mathbb Z}$ and $y\in \mathord {\mathbb N}$ , then both are of type integer ( $\mathord {\mathbb Z}$ ). $\mathord {\mathbb N}$ is not another type. There is just the additional condition $y \geq 0$ .

Rodin Handbook

2.5.6 Arithmetic