theorem Th5: :: PRGCOR_1:5

for n, k being Element of NAT st k > 0 & n mod (2 * k) < k holds
n div k = (n div (2 * k)) * 2