theorem :: INT_8:19

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