Solution (source code)

= Solution

A <Euclidean domain> is an <integral domain> $R$ with a function $\delta:R\setminus\{0\}\to\mathbb Z_{\ge0}$ such that, for every $a\in R$ and nonzero $b\in R$, there are $q,r\in R$ satisfying $a=bq+r$, with either $r=0$ or $\delta(r)<\delta(b)$.

For the <integers>, take $\delta(b)=|b|$. Given $a$ and $b\ne0$, put $m=|b|$ and choose the integer $q_0=\lfloor a/m\rfloor$. Then $a=mq_0+r$ with $0\le r<m$. Setting $q=q_0$ when $b>0$ and $q=-q_0$ when $b<0$ gives $a=bq+r$. A nonzero remainder has $\delta(r)=r<|b|=\delta(b)$, and the <integers> are an <integral domain>. Thus \b[$\mathbb Z$ is a Euclidean domain with Euclidean function $|b|$].