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

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