let n be Nat; :: thesis: [/(((2 * n) + 1) / 2)\] = n + 1
(2 * n) + 1 <= ((2 * n) + 1) + 1 by NAT_1:11;
then (2 * n) + 1 <= 2 * (n + 1) ;
then A1: ((2 * n) + 1) / 2 <= n + 1 by XREAL_1:79;
2 * n < (2 * n) + 1 by NAT_1:13;
then n + 1 < (((2 * n) + 1) / 2) + 1 by XREAL_1:6, XREAL_1:81;
hence [/(((2 * n) + 1) / 2)\] = n + 1 by A1, INT_1:def 7; :: thesis: verum