let n be natural odd number ; :: thesis: n div 2 = (n - 1) / 2
consider k being Integer such that
A1: n = (2 * k) + 1 by ABIAN:1;
A2: (n - 1) / 2 = k by A1;
(n - 1) + 1 = n ;
then n - 1 <= n by INT_1:6;
then A3: k <= n / 2 by A2, XREAL_1:72;
(n / 2) - (1 / 2) > (n / 2) - 1 by XREAL_1:10;
hence n div 2 = (n - 1) / 2 by A1, A3, INT_1:def 6; :: thesis: verum