let a, b, n be Nat; :: thesis: ( ( a <> 0 or b <> 0 ) & n > 0 & a divides (b |^ n) - 1 implies a,b are_coprime )
set g = a gcd b;
assume ( ( a <> 0 or b <> 0 ) & n > 0 & a divides (b |^ n) - 1 ) ; :: thesis: a,b are_coprime
then ( a gcd b divides b |^ n & a gcd b divides (b |^ n) - 1 ) by INT_2:2, INT_2:21, NEWTON02:14;
then a gcd b divides (b |^ n) - ((b |^ n) - 1) by INT_5:1;
hence a,b are_coprime by WSIERP_1:15; :: thesis: verum