## Two copies of Nat

With our construction of $\mathbb{Z}$, we (eventually) get two copies of $\mathbb{N}$ one coming from the function \(i : \mathbb{N} \to \mathbb{Z}\) and the other from \(j : \mathbb{N} \to \mathbb{Z}\)

We can think of one copy of $\mathbb{N}$ as the non-negative integers and the other as the non-positive integers – with their overlap being $0$.

One can could imagine building an inductive type from this expressing that we have two ways to build an integer from a natural number. Indeed, that is what Lean does but a slight shift. The two copies of `Nat`

in `Int`

are the non-negative integers and the *strictly* negative integers.

`negSucc n`

should be viewed as `-n-1`

. Lean gives the analog of $j$ above as

In Grothendieck construction of $\mathbb{Z}$, we got addition almost immediately since it was natural to add $\mathbb{N} \times \mathbb{N}$. In Lean, it requires a bit more book-keeping using successors when using `negSucc`

.

This uses `subNatNat`

(read as subtract a natural number from a natural number).

Natural number subtraction returns `0`

if `m ≥ n`

.

On the other hand, perhaps multiplication looks simpler than the formula we had before.