for a being Nat
for t being Integer holds
( not |.t.| < a or t mod a = |.t.| or t mod a = a - |.t.| )