Definition  We define:
ℕ :=: {(0)(n+1) | n ∈ ℕ}
(m+1) = (n+1)  :⇔  m = n  (m ∈ ℕ, n ∈ ℕ)

The set of natural numbers is defined as a construction with two constructors, which, in this case, exactly matches the corresponding definition of an inductive data type. We merely use a custom notation for the "successor" constructor, but we could just as well write "S(n)". The notation is justified by $"Addition of one yields successor".

In this library, the natural numbers start at 0, which is known to be far more convenient than starting at 1.