theorem MRS: :: NEWTON06:51

for a, b being non zero Nat holds (a - b) mod (2 * b) = (a + b) mod (2 * b)