theorem :: NAT_D:2

for i, j being natural Number st 0 < i holds
j = (i * (j div i)) + (j mod i) by INT_1:59;