let n be even Integer; :: thesis: for m being odd Integer st n <= m holds
n + 1 <= m
let m be odd Integer; :: thesis: ( n <= m implies n + 1 <= m )
assume A1: n <= m ; :: thesis: n + 1 <= m
consider k1 being Integer such that
A2: n = 2 * k1 by ABIAN:11;
consider k2 being Integer such that
A3: m = (2 * k2) + 1 by ABIAN:1;
per cases ( k1 <= k2 or k1 > k2 ) ;
suppose k1 <= k2 ; :: thesis: n + 1 <= m
then 2 * k1 <= 2 * k2 by XREAL_1:64;
hence n + 1 <= m by A2, A3, XREAL_1:6; :: thesis: verum
end;
suppose k1 > k2 ; :: thesis: n + 1 <= m
then k2 + 1 <= k1 by INT_1:7;
then 2 * (k2 + 1) <= 2 * k1 by XREAL_1:64;
then (2 * k2) + 2 <= (2 * k2) + 1 by A1, A2, A3, XXREAL_0:2;
hence n + 1 <= m by XREAL_1:6; :: thesis: verum
end;
end;