theorem Th9: :: NUMBER16:9

for n, k being Nat st k < n & n <= 7 holds
ex i being Nat st (Fib i) mod n = k