for p being Nat
for a being Integer holds ((a * p) + 1) mod p = 1 mod p