let n be even Integer; :: thesis: for m being odd Integer st m <= n holds
m + 1 <= n
let m be odd Integer; :: thesis: ( m <= n implies m + 1 <= n )
assume A1: m <= n ; :: thesis: m + 1 <= n
consider k1 being Integer such that
A2: n = 2 * k1 by ABIAN:11;
consider k2 being Integer such that
A3: m + 1 = 2 * k2 by ABIAN:11;

per cases ( k2 <= k1 or k2 > k1 ) ;

suppose k2 <= k1 ; :: thesis: m + 1 <= n

hence m + 1 <= n by A2, A3, XREAL_1:64; :: thesis: verum

end;

suppose k2 > k1 ; :: thesis: m + 1 <= n

then k1 + 1 <= k2 by INT_1:7;
then A4: 2 * (k1 + 1) <= 2 * k2 by XREAL_1:64;
m + 1 <= (2 * k1) + 1 by A1, A2, XREAL_1:6;
then (2 * k1) + 2 <= (2 * k1) + 1 by A3, A4, XXREAL_0:2;
hence m + 1 <= n by XREAL_1:6; :: thesis: verum

end;

end;