theorem :: NEWTON05:12

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