let a, b, k, m be Nat; :: thesis: ( a |^ (k + 1),b |^ (m + 1) are_coprime implies a,b are_coprime )
( a |^ (k + 1) = a * (a |^ k) & b |^ (m + 1) = b * (b |^ m) ) by NEWTON:6;
hence ( a |^ (k + 1),b |^ (m + 1) are_coprime implies a,b are_coprime ) by Th40; :: thesis: verum