per
cases
(
0
<=
x
or
x
<
0
)
;
suppose
A1
:
0
<=
x
;
:: thesis:
not
.
x
.
is
negative
then
.
x
.
=
x
by
Def1
;
hence
not
.
x
.
is
negative
by
A1
;
:: thesis:
verum
end;
suppose
A2
:
x
<
0
;
:: thesis:
not
.
x
.
is
negative
then
.
x
.
=

x
by
Def1
;
hence
not
.
x
.
is
negative
by
A2
;
:: thesis:
verum
end;
end;