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;