:: deftheorem defines are_congruent_mod INT_1:def 4 :
for i1, i2, i3 being Integer holds
( i1,i2 are_congruent_mod i3 iff i3 divides i1 - i2 );