reconsider i = 2 -root a as Integer ;
( (i ^2) mod 4 = 0 * 0 or (i ^2) mod 4 = 1 * 1 ) by PYTHTRIP:3, PYTHTRIP:4;
hence a mod 4 is square ; :: thesis: verum