Solution (source code)

= Solution

A <Euclidean domain> is an <integral domain> $R$ admitting a <Euclidean function> $\delta:R\setminus\{0\}\to\mathbb Z_{\geq0}$ such that division with a smaller remainder is possible: for every $a\in R$ and nonzero $b\in R$, there are $q,r\in R$ with
$$
\boxed{a=qb+r,\qquad r=0\ \text{or}\ \delta(r)<\delta(b).}
$$
Thus the <Euclidean function> measures progress in repeated division. Definitions which additionally normalize it to be nondecreasing under multiplication give the same class of <Euclidean domains>; the division property is the one needed below.