for a, b being Nat
for c being non zero Nat holds
( (a mod c) * (b mod c) < c iff (a * b) mod c = (a mod c) * (b mod c) )