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