theorem Th3: :: PRGCOR_1:3

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