for a, b, n being Nat st a,b are_coprime holds
a * b,(a |^ (n + 1)) - (b |^ (n + 1)) are_coprime