theorem Th88: :: NEWTON02:186

for n being Nat holds
( 2 divides (2 |^ n) - 1 iff n = 0 )