theorem Th2: :: PRGCOR_1:2

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