theorem MAB: :: NEWTON05:19

for a, b being Integer
for c being non zero Nat holds
( ( (a + b) mod c = b mod c implies a mod c = 0 ) & ( (a + b) mod c <> b mod c implies a mod c > 0 ) )