per
cases
(
n
=
0
or
n
<>
0
)
;
suppose
n
=
0
;
:: thesis:
Lucas
n
is
positive
hence
Lucas
n
is
positive
by
Th11
;
:: thesis:
verum
end;
suppose
n
<>
0
;
:: thesis:
Lucas
n
is
positive
hence
Lucas
n
is
positive
by
Th17
;
:: thesis:
verum
end;
end;