The natural numbers, represented as the first ordinal numbers. The number zero is the empty set, the successor operation is succ. The inherent induction principle is shown by onat_induction_sets and onat_induction.