let n, k be Element of NAT ; :: thesis: ( k > 0 & n mod (2 * k) >= k implies n div k = ((n div (2 * k)) * 2) + 1 )
assume that
A1: k > 0 and
A2: n mod (2 * k) >= k ; :: thesis: n div k = ((n div (2 * k)) * 2) + 1
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
.= ((2 * k) * (n div (2 * k))) + ((n mod k) + k) by A1, A2, Th2
.= (k * ((2 * (n div (2 * k))) + 1)) + (n mod k) ;
n mod k < k by A1, NAT_D:1;
hence n div k = ((n div (2 * k)) * 2) + 1 by A3, NAT_D:def 1; :: thesis: verum