let k, n be Nat; :: thesis: ( k <= 2 * n implies (k + 1) div 2 <= n )
assume k <= 2 * n ; :: thesis: (k + 1) div 2 <= n
then k + 1 <= (2 * n) + 1 by XREAL_1:6;
then (k + 1) div 2 <= ((2 * n) + 1) div 2 by Th24;
hence (k + 1) div 2 <= n by NAT_D:def 1; :: thesis: verum