for i1, i2, i3 being Integer st i1,i2 are_congruent_mod i3 holds
i1 gcd i3 = i2 gcd i3