let n, k be Element of NAT ; :: thesis: ( k > 0 & n mod (2 * k) < k implies n div k = (n div (2 * k)) * 2 )
assume that
A1: k > 0 and
A2: n mod (2 * k) < k ; :: thesis: n div k = (n div (2 * k)) * 2
2 * k > 2 * 0 by A1, XREAL_1:68;
then A3: n = ((2 * k) * (n div (2 * k))) + (n mod (2 * k)) by NAT_D:2
.= (k * (2 * (n div (2 * k)))) + (n mod k) by A2, Th4 ;
n mod k < k by A1, NAT_D:1;
hence n div k = (n div (2 * k)) * 2 by A3, NAT_D:def 1; :: thesis: verum