let i0, i1 be Integer; :: thesis: ( i0 < i1 implies i0 + 1 <= i1 )
assume i0 < i1 ; :: thesis: i0 + 1 <= i1
then i0 + (- i0) < i1 + (- i0) by XREAL_1:6;
then 1 <= i1 + (- i0) by Lm4;
then 1 + i0 <= (i1 + (- i0)) + i0 by XREAL_1:6;
hence i0 + 1 <= i1 ; :: thesis: verum