theorem CoprimeProof: :: NUMBER18:70

for m being non zero Nat holds (2 |^ m) - 1,(((2 |^ m) - 1) |^ m) - 1 are_coprime