theorem Th13: :: NUMBER16:13

( Fib 0, Fib 12 are_congruent_mod 8 & Fib 1, Fib (12 + 1) are_congruent_mod 8 & ( for x being Nat st x < 12 holds
( (Fib x) mod 8 <> 4 & (Fib x) mod 8 <> 6 ) ) )