theorem XLMOD04: :: AESCIP_1:6

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