for i, j being Integer st i,j are_coprime holds
ex s being Integer st s * i,1 are_congruent_mod j