theorem :: NEWTON05:13

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