Natural numbers

A definition

inductive nat : Type
| zero : nat
| succ : nat → nat