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