for i, j being natural Number holds
( j divides i iff i = j * (i div j) )