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;