theorem :: INT_2:15

for a, b, c being Integer holds
( a,b are_congruent_mod c iff c divides a - b ) ;