Definition 1.8.1.1. We define:

ℕ :=: {(0)(*n*+1) | *n* ∈ ℕ}

(*m*+1) = (*n*+1) :⇔ *m* = *n* (*m* ∈ ℕ, *n* ∈ ℕ)

Remarks.

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.

References.

- https://en.wikipedia.org/wiki/Natural_number
- https://mathworld.wolfram.com/NonnegativeInteger.html
- https://proofwiki.org/wiki/Definition:Natural_Numbers
- https://ncatlab.org/nlab/show/natural+number
- https://coq.inria.fr/library/Coq.Init.Nat.html
- https://coq.inria.fr/library/Coq.NArith.BinNat.html
- https://leanprover-community.github.io/mathlib_docs/init/core.html#nat
- http://oeis.org/A001477