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

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

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

then A2: i1 -' n = i1 - n by XREAL_0:def 2;
i1 - n <= i2 - n by A1, XREAL_1:9;
hence i1 -' n <= i2 -' n by A2, XREAL_0:def 2; :: thesis: verum

end;

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

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

end;

end;