theorem Th12: :: NUMBER16:12

for i, j, k being Nat st 0 < j & k < i & ( for x, y being Nat st x,y are_congruent_mod j holds
Fib x, Fib y are_congruent_mod i ) & ( for x being Nat st x < j holds
(Fib x) mod i <> k ) holds
for m being Nat holds not (ArProg (k,i)) . m is Fibonacci