for i, p being Nat st p is prime & i,p are_coprime holds
order (i,p) divides p -' 1