theorem XLMOD01X: :: AESCIP_1:4

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