Three Squares Theorem

We formalize the Legendre's three squares theorem and its consequences, in particular the following results:

1. A natural number can be represented as the sum of three squares of natural numbers if and only if it is not of the form $4^a(8k+7)$, where $a$ and $k$ are natural numbers.
2. If $n$ is a natural number such that $n\equiv 3(\mathrm{mod}8)$, then $n$ can be be represented as the sum of three squares of odd natural numbers.

Consequences include the following:

1. An integer $n$ can be written as $n=x^2+y^2+z^2+z$, where $x$, $y$, $z$ are integers, if and only if $n\ge 0$.
2. The Legendre's four squares theorem: any natural number can be represented as the sum of four squares of natural numbers.