theorem DIM: :: NEWTON06:27

for a being non zero Integer
for b being Integer holds
( a divides b iff a divides b mod a )