per cases ( a is odd or a is even ) ;

suppose a is odd ; :: thesis: a mod 8 is square

then a mod 8 = 1 * 1 by MOD8;
hence a mod 8 is square ; :: thesis: verum

end;

suppose a is even ; :: thesis: a mod 8 is square

then reconsider k = a / 4 as Nat ;

per cases ( k is odd or k is even ) ;

suppose k is odd ; :: thesis: a mod 8 is square

then reconsider m = (k - 1) / 2 as Nat ;
((2 * m) + 1) mod 2 = 1 ;
then (4 * k) mod (4 * 2) = 4 * 1 by INT_4:20
.= 2 * 2 ;
hence a mod 8 is square ; :: thesis: verum

end;

suppose k is even ; :: thesis: a mod 8 is square

then k mod 2 = 0 ;
then (4 * k) mod (4 * 2) = 4 * 0 by INT_4:20
.= 0 * 0 ;
hence a mod 8 is square ; :: thesis: verum

end;

end;

end;

end;