theorem R3: :: NEWTON06:66

for a, b being Integer holds a mod b = b * (frac (a / b))