theorem :: INT_8:16

for i, s, t, n being Nat st n > 1 & i,n are_coprime & order (i,n) = s * t holds
order ((i |^ s),n) = t