A1: for n, k being Nat st k >= 1 holds
uInt . n < uInt . (n + k)

proof

let n be Nat; :: thesis: for k being Nat st k >= 1 holds
uInt . n < uInt . (n + k)
defpred S₁[ Nat] means uInt . n < uInt . (n + $1);
A2: S₁[1] by Lm1;
A3: for j being Nat st 1 <= j & S₁[j] holds
S₁[j + 1]

proof

let j be Nat; :: thesis: ( 1 <= j & S₁[j] implies S₁[j + 1] )
assume A4: ( 1 <= j & S₁[j] ) ; :: thesis: S₁[j + 1]
uInt . (n + j) <= uInt . ((n + j) + 1) by Lm1;
hence S₁[j + 1] by A4, SURREALO:4; :: thesis: verum

end;

for j being Nat st 1 <= j holds
S₁[j] from NAT_1:sch 8(A2, A3);
hence for k being Nat st k >= 1 holds
uInt . n < uInt . (n + k) ; :: thesis: verum

end;

A5: for n, k being Nat st k >= 1 holds
uInt . (- (n + k)) < uInt . (- n)

proof

let n be Nat; :: thesis: for k being Nat st k >= 1 holds
uInt . (- (n + k)) < uInt . (- n)
defpred S₁[ Nat] means uInt . (- (n + $1)) < uInt . (- n);
A6: S₁[1] by Lm2;
A7: for j being Nat st 1 <= j & S₁[j] holds
S₁[j + 1]

proof

let j be Nat; :: thesis: ( 1 <= j & S₁[j] implies S₁[j + 1] )
assume A8: ( 1 <= j & S₁[j] ) ; :: thesis: S₁[j + 1]
uInt . (- ((n + j) + 1)) <= uInt . (- (n + j)) by Lm2;
hence S₁[j + 1] by A8, SURREALO:4; :: thesis: verum

end;

for j being Nat st 1 <= j holds
S₁[j] from NAT_1:sch 8(A6, A7);
hence for k being Nat st k >= 1 holds
uInt . (- (n + k)) < uInt . (- n) ; :: thesis: verum

end;

let i, j be Integer; :: thesis: ( i < j implies uInt . i < uInt . j )
assume A9: i < j ; :: thesis: uInt . i < uInt . j
i in INT by INT_1:def 2;
then consider I being Nat such that
A10: ( i = I or i = - I ) by INT_1:def 1;
j in INT by INT_1:def 2;
then consider J being Nat such that
A11: ( j = J or j = - J ) by INT_1:def 1;

per cases ( ( i = I & j = J ) or ( i = I & j = - J ) or ( i = - I & j = J ) or ( i = - I & j = - J ) ) by A10, A11;

suppose A12: ( i = I & j = J ) ; :: thesis: uInt . i < uInt . j

then reconsider JI = J - I as Nat by A9, NAT_1:21;
JI <> 0 by A12, A9;
then uInt . I < uInt . (I + JI) by A1, NAT_1:14;
hence uInt . i < uInt . j by A12; :: thesis: verum

end;

suppose ( i = I & j = - J ) ; :: thesis: uInt . i < uInt . j

hence uInt . i < uInt . j by A9; :: thesis: verum

end;

suppose A13: ( i = - I & j = J ) ; :: thesis: uInt . i < uInt . j

per cases ( i = 0 or j = 0 or ( i <> 0 & j <> 0 ) ) ;

suppose A14: i = 0 ; :: thesis: uInt . i < uInt . j

then uInt . 0 < uInt . (0 + j) by A9, A1, NAT_1:14;
hence uInt . i < uInt . j by A14; :: thesis: verum

end;

suppose A15: j = 0 ; :: thesis: uInt . i < uInt . j

then uInt . (- (0 + I)) < uInt . (- 0) by A9, A13, A5, NAT_1:14;
hence uInt . i < uInt . j by A15, A13; :: thesis: verum

end;

suppose ( i <> 0 & j <> 0 ) ; :: thesis: uInt . i < uInt . j

then ( uInt . (- (0 + I)) < uInt . (- 0) & uInt . (- 0) <= uInt . (0 + J) ) by A13, NAT_1:14, A1, A5;
hence uInt . i < uInt . j by A13, SURREALO:4; :: thesis: verum

end;

end;

end;

suppose A16: ( i = - I & j = - J ) ; :: thesis: uInt . i < uInt . j

then reconsider IJ = I - J as Nat by A9, XREAL_1:24, NAT_1:21;
IJ <> 0 by A16, A9;
then uInt . (- (J + IJ)) < uInt . (- J) by A5, NAT_1:14;
hence uInt . i < uInt . j by A16; :: thesis: verum

end;

end;