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

per cases ( i2 <= n or i2 > n ) ;

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

then A3: n -' i1 = n - i1 by A1, XREAL_1:233, XXREAL_0:2;
n -' i2 = n - i2 by A2, XREAL_1:233;
hence n -' i2 <= n -' i1 by A1, A3, XREAL_1:10; :: thesis: verum

end;

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

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

end;

end;