Construction of the Integers: Pairs of Natural Numbers up to Equal Differences, with Sum, Product, Negation and Order

In the setting of The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion, let $P=\mathbb{N}\times\mathbb{N}$ and let $\sim$ be the relation on $P$ with $(a,b)\sim(c,d)$ if and only if $a+d=b+c$, for all $a,b,c,d\in\mathbb{N}$, given by Maps and Relations Given by Formulas §relation.

¶ $\sim$ is an equivalence relation on $P$. Write $P/{\sim}$ for the quotient and $[a,b]$ for the class of $(a,b)$.

¶ $P/{\sim}$ is a set whose elements are exactly the classes $[a,b]$ with $a,b\in\mathbb{N}$, and for all $a,b,c,d\in\mathbb{N}$, $[a,b]=[c,d]$ if and only if $a+d=b+c$.

¶ There are unique binary operations $+$ and $\cdot$ on $P/{\sim}$, a unique map $x\mapsto-x$ from $P/{\sim}$ to itself and a unique relation $\le$ on $P/{\sim}$ such that, for all $a,b,c,d\in\mathbb{N}$,

$$[a,b]+[c,d]=[a+c,b+d],\quad[a,b]\cdot[c,d]=[ac+bd,ad+bc],\quad-[a,b]=[b,a],\quad[a,b]\le[c,d]\iff a+d\le b+c.$$