theorem Th45: :: NUMBER03:45
for a, b, n being Nat st ( a <> 0 or b <> 0 ) & n > 0 & a divides (b |^ n) - 1 holds
a,b are_coprime