for n being non zero Nat
for i being Integer holds (i * n) mod n = 0 by NAT_D:71;