( b = 0 or b mod (a * b) = b - ((b div (a * b)) * (a * b)) ) by INT_1:def 10;
hence b mod (a * b) = b ; :: thesis: verum