mathlib3

feat(number_theory/sum_two_squares): fermat's theorem on sums of two squares

#776

Merged