let n be Nat; :: thesis: ( not n divides 4 or n = 1 or n = 2 or n = 4 )
assume A1: n divides 4 ; :: thesis: ( n = 1 or n = 2 or n = 4 )
then n <= 4 by INT_2:27;
then A2: not not n = 0 & ... & not n = 4 ;

now :: thesis: not 3 divides 4

((3 * 1) + 1) mod 3 = 1 mod 3 by NAT_D:21
.= 1 by NAT_D:24 ;
hence not 3 divides 4 by INT_1:62; :: thesis: verum

end;

hence ( n = 1 or n = 2 or n = 4 ) by A1, A2; :: thesis: verum