mathlib3

feat(number_theory/sum_four_squares): every natural number is the sum of four square numbers

#1560

Merged