theorem :: NEWTON02:191

for b being Nat holds not 3 divides (((b |^ 3) + (b |^ 2)) - b) + 1