theorem XLMOD01: :: AESCIP_1:2

for k, m being Nat st m <> 0 & (k + 1) mod m <> 0 holds
(k + 1) div m = k div m