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

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