let a, b be Nat; :: thesis: ( a <= b implies a -' 1 <= b -' 1 )
assume AS: a <= b ; :: thesis: a -' 1 <= b -' 1

per cases ( a = 0 or a > 0 ) ;

suppose a = 0 ; :: thesis: a -' 1 <= b -' 1

then a - 1 = - 1 ;
hence a -' 1 <= b -' 1 by XREAL_0:def 2; :: thesis: verum

end;

suppose a > 0 ; :: thesis: a -' 1 <= b -' 1

then ( a -' 1 = a - 1 & b -' 1 = b - 1 ) by AS, XREAL_0:def 2;
hence a -' 1 <= b -' 1 by AS, XREAL_1:9; :: thesis: verum

end;

end;