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