let n, k be Element of NAT ; :: thesis: ( k > 0 & n mod (2 * k) < k implies n mod (2 * k) = n mod k )
assume that
A1: k > 0 and
A2: n mod (2 * k) < k ; :: thesis: n mod (2 * k) = n mod k
( ex t being Nat st
( n = ((2 * k) * t) + (n mod (2 * k)) & n mod (2 * k) < 2 * k ) or ( n mod (2 * k) = 0 & 2 * k = 0 ) ) by NAT_D:def 2;
then consider t being Nat such that
A3: n = ((2 * k) * t) + (n mod (2 * k)) by A1;
reconsider t = t as Element of NAT by ORDINAL1:def 12;
n = (k * (2 * t)) + (n mod (2 * k)) by A3;
hence n mod (2 * k) = n mod k by A2, NAT_D:def 2; :: thesis: verum