theorem :: NEWTON02:164

for a being Nat st not 7 divides a holds
7 divides (a |^ 6) - 1