for x, y, n being Integer st x,n are_coprime & x,y are_congruent_mod n holds
y,n are_coprime