theorem :: NUMBER02:33

for n being Nat holds
( not 5 divides n iff ex k being Nat st
( n = (5 * k) + 1 or n = (5 * k) + 2 or n = (5 * k) + 3 or n = (5 * k) + 4 ) )