let a, b be Integer; :: thesis: ( 0 < b & a divides b implies a <= b )
assume A1: 0 < b ; :: thesis: ( not a divides b or a <= b )
assume a divides b ; :: thesis: a <= b
then consider c being Integer such that
A2: b = a * c ;

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

suppose a <= 0 ; :: thesis: a <= b

hence a <= b by A1; :: thesis: verum

end;

suppose A3: a > 0 ; :: thesis: a <= b

then c > 0 by A1, A2;
then c >= 0 + 1 by INT_1:7;
hence a <= b by A2, A3, XREAL_1:151; :: thesis: verum

end;

end;