for a, m being Nat st a <> 0 & m <> 0 & a,m are_coprime holds
for b being Nat holds a |^ b,m are_coprime