for m, n, l being Nat holds (l * m) mod n = (l * (m mod n)) mod n