theorem :: INT_3:3

for a, b being Element of INT.Ring st b <> 0. INT.Ring holds
a = ((a div b) * b) + (a mod b) by INT_1:59;