lean_workbook_plus_11123

Consider the equation modulo 4. We have $x^{2}\equiv-y\pmod{4}$ . Since $x^2$ can be congruent to only 0 or 1 mod 4, $y$ is congruent to 0 or -1 mod 4.