# mathlibdocumentation

number_theory.sum_four_squares

# Lagrange's four square theorem #

The main result in this file is sum_four_squares, a proof that every natural number is the sum of four square numbers.

## Implementation Notes #

The proof used is close to Lagrange's original proof.

theorem int.sq_add_sq_of_two_mul_sq_add_sq {m x y : } (h : 2 * m = x ^ 2 + y ^ 2) :
m = ((x - y) / 2) ^ 2 + ((x + y) / 2) ^ 2