for m being Nat
for i being Integer st m divides i holds
i div m divides i