theorem :: NEWTON02:170

for a being Nat holds
( 5 divides (a |^ 3) - 1 iff 5 divides a - 1 )