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.