theorem :: NEWTON02:99

for m being Nat holds
( (2 |^ m) - 1 divides (2 |^ ((2 * m) + 1)) - 2 & (2 |^ m) + 1 divides (2 |^ ((2 * m) + 1)) - 2 )