let i1, i2 be natural Number ; :: thesis: ( ( i1 < i2 or i1 + 1 <= i2 ) implies i1 <= i2 -' 1 )
assume A1: ( i1 < i2 or i1 + 1 <= i2 ) ; :: thesis: i1 <= i2 -' 1

per cases ( i1 < i2 or i1 + 1 <= i2 ) by A1;

suppose A2: i1 < i2 ; :: thesis: i1 <= i2 -' 1

then i1 + 1 <= i2 by NAT_1:13;
then A3: (i1 + 1) - 1 <= i2 - 1 by XREAL_1:9;
0 + 1 <= i2 by A2, NAT_1:13;
hence i1 <= i2 -' 1 by A3, XREAL_1:233; :: thesis: verum

end;

suppose A4: i1 + 1 <= i2 ; :: thesis: i1 <= i2 -' 1

then A5: (i1 + 1) - 1 <= i2 - 1 by XREAL_1:9;
0 + 1 <= i2 by A4, NAT_1:13;
hence i1 <= i2 -' 1 by A5, XREAL_1:233; :: thesis: verum

end;

end;