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;