let n, m be odd Integer; :: thesis: ( n < m implies n <= m - 2 )
assume n < m ; :: thesis: n <= m - 2
then n + 1 <= m by INT_1:7;
then (n + 1) + (- 1) <= m + (- 1) by XREAL_1:7;
then n < m - 1 by XXREAL_0:1;
then n + 1 <= m - 1 by INT_1:7;
then (n + 1) + (- 1) <= (m - 1) + (- 1) by XREAL_1:7;
hence n <= m - 2 ; :: thesis: verum