theorem :: INT_8:11

for s, i, n being Nat st n > 1 & i,n are_coprime holds
( i |^ s,1 are_congruent_mod n iff order (i,n) divides s )