for i, m, n being Nat st n > 1 & m > 1 & i,n are_coprime & m divides n holds
order (i,m) divides order (i,n)