let i1, i2 be natural Number ; :: thesis: ( i1 <= i2 implies i1 -' 1 <= i2 )
assume A1: i1 <= i2 ; :: thesis: i1 -' 1 <= i2
reconsider i1 = i1, i2 = i2 as Nat by TARSKI:1;

per cases ( i1 - 1 >= 0 or i1 - 1 < 0 ) ;

suppose i1 - 1 >= 0 ; :: thesis: i1 -' 1 <= i2

then i1 -' 1 = i1 - 1 by XREAL_0:def 2;
then i1 -' 1 <= (i1 - 1) + 1 by NAT_1:12;
hence i1 -' 1 <= i2 by A1, XXREAL_0:2; :: thesis: verum

end;

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

hence i1 -' 1 <= i2 by XREAL_0:def 2; :: thesis: verum

end;

end;