theorem Th4: :: PRGCOR_1:4

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