theorem INT162: :: NEWTON06:6

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