The Natural Numbers with Zero as a Type

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, with $\mathbb{N}_{0}$, $0$ and $1$ as in The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion (ii):

(i) The type. $\mathrm{Natural}$ is the type whose elements are the natural numbers with zero: an element of $\mathrm{Natural}$ is a set $n\in\mathbb{N}_{0}$, carried with the fact that it lies in $\mathbb{N}_{0}$, and two elements are equal when their sets are (the one place where a natural number is handled as a set, as a type requires).

(ii) Operations. The elements $0$ and $1$, the operations $a+b$ and $a\cdot b$ and the relations $a\le b$ and $a<b$ of $\mathrm{Natural}$ are those of $\mathbb{N}_{0}$: the sets of $0$ and $1$ are $0$ and $1$; the set of $a+b$ is the sum of the sets of $a$ and $b$ under the addition, which lies in $\mathbb{N}_{0}$ by that definition; the set of $a\cdot b$ is their product under the multiplication, which also lies in $\mathbb{N}_{0}$; and $a\le b$, respectively $a<b$, holds when the sets of $a$ and $b$ are related by the order, respectively the strict order, of $\mathbb{N}_{0}$. In particular the set of $a+1$ is the successor of the set of $a$, by Natural Numbers Are the Successors in Omega: One Is Least and Not a Successor of a Natural Number, the Successor Is Injective, and N Is Closed under Addition and Multiplication (v).

(iii) Numerals. Numerals $k$ (natural numbers of the ambient mathematics, not elements of $\mathbb{N}_{0}$) and powers are read recursively: the numeral $0$ is read as $0$, $1$ as $1$ and $k+2$ as $(k+1)+1$; $a^{0}=1$ and $a^{k+1}=a^{k}\cdot a$; and $k\cdot a$ is the product of the reading of $k$ with $a$.

Since an element of $\mathrm{Natural}$ is determined by its set, the laws of $\mathbb{N}_{0}$ hold for these operations and this order; below, $a$, $b$ and $c$ are elements of $\mathrm{Natural}$.

(iv) Commutative semiring. The laws of a commutative semiring hold:

$$(a+b)+c=a+(b+c),\quad a+b=b+a,\quad a+0=a,\quad (a\cdot b)\cdot c=a\cdot(b\cdot c),\quad a\cdot b=b\cdot a,\quad a\cdot1=1\cdot a=a,$$ $$a\cdot0=0\cdot a=0,\quad a\cdot(b+c)=a\cdot b+a\cdot c,\quad (a+b)\cdot c=a\cdot c+b\cdot c$$

(Arithmetic of Addition on Omega: Recursion Rules, Associativity, Commutativity, Cancellation and Compatibility with the Order (iii), Arithmetic of Addition on Omega: Recursion Rules, Associativity, Commutativity, Cancellation and Compatibility with the Order (iv), Arithmetic of Addition on Omega: Recursion Rules, Associativity, Commutativity, Cancellation and Compatibility with the Order (i), Arithmetic of Multiplication on Omega: Recursion Rules, Distributivity, Associativity, Commutativity, No Zero Divisors, Cancellation and Compatibility with the Order (v), Arithmetic of Multiplication on Omega: Recursion Rules, Distributivity, Associativity, Commutativity, No Zero Divisors, Cancellation and Compatibility with the Order (vi), Arithmetic of Multiplication on Omega: Recursion Rules, Distributivity, Associativity, Commutativity, No Zero Divisors, Cancellation and Compatibility with the Order (iii) as $1$ is the successor of $0$ by The Set of Natural Numbers and the Number One (ii), Arithmetic of Multiplication on Omega: Recursion Rules, Distributivity, Associativity, Commutativity, No Zero Divisors, Cancellation and Compatibility with the Order (i), Arithmetic of Multiplication on Omega: Recursion Rules, Distributivity, Associativity, Commutativity, No Zero Divisors, Cancellation and Compatibility with the Order (iv)); and the reading of a numeral $k+1$ is the reading of $k$ plus $1$ (for $k=0$ because $0+1=1$).

(v) Cancellation. Addition cancels on both sides: $a+c=b+c$ implies $a=b$, and $c+a=c+b$ implies $a=b$ (Arithmetic of Addition on Omega: Recursion Rules, Associativity, Commutativity, Cancellation and Compatibility with the Order (v), with Arithmetic of Addition on Omega: Recursion Rules, Associativity, Commutativity, Cancellation and Compatibility with the Order (iv)).

(vi) Order. $\le$ on $\mathrm{Natural}$ is reflexive, antisymmetric, transitive and total, as $\le$ is a well-order on $\mathbb{N}_{0}$ (The Order on Omega Is a Well-Order with Membership as Its Strict Order, and Nothing Lies between n and Its Successor (i)) and hence a total order (Well-Orders on a Set (i)); $a<b$ holds exactly when $a\le b$ and not $b\le a$ (The Order on Omega Is a Well-Order with Membership as Its Strict Order, and Nothing Lies between n and Its Successor (ii), with antisymmetry); and

$$0\le a,\qquad a<a+1,\qquad a<b\iff a+1\le b$$

(The Order on Omega Is a Well-Order with Membership as Its Strict Order, and Nothing Lies between n and Its Successor (iii), The Order on Omega Is a Well-Order with Membership as Its Strict Order, and Nothing Lies between n and Its Successor (iv) and The Order on Omega Is a Well-Order with Membership as Its Strict Order, and Nothing Lies between n and Its Successor (vi), as $a+1$ is the successor of $a$ by Natural Numbers Are the Successors in Omega: One Is Least and Not a Successor of a Natural Number, the Successor Is Injective, and N Is Closed under Addition and Multiplication (v)).

(vii) Order and addition. $a\le b$ if and only if $a+c\le b+c$ (Arithmetic of Addition on Omega: Recursion Rules, Associativity, Commutativity, Cancellation and Compatibility with the Order (vi), with Arithmetic of Addition on Omega: Recursion Rules, Associativity, Commutativity, Cancellation and Compatibility with the Order (iv)), and $a\le b$ if and only if $b=a+c$ for some $c$ (Arithmetic of Addition on Omega: Recursion Rules, Associativity, Commutativity, Cancellation and Compatibility with the Order (vii)); in particular $a\le a+b$, and if $a<b$ then $b=a+c$ for some $c$ with $0<c$ (take $c=1+d$, where $b=(a+1)+d$ as $a+1\le b$; then $0<c$ by (vi), as $0+1=1\le 1+d$).

In Lean these clauses are the classes $\mathtt{Lean.Grind.CommSemiring}$; $\mathtt{Lean.Grind.AddRightCancel}$; $\mathtt{Std.IsLinearOrder}$ and $\mathtt{Std.LawfulOrderLT}$; and $\mathtt{Lean.Grind.OrderedAdd}$ and $\mathtt{Lean.Grind.ExistsAddOfLT}$.