for a being Nat
for t, u being Integer holds (- t) mod a = ((u * a) - (t mod a)) mod a