theorem XLMOD03: :: AESCIP_1:5

for k, m being Nat holds (k - m) mod m = k mod m