But it doesn’t seem necessary I think. We could just modify these lines to include 0 <= n instead of 0 < n:
0 <= n
0 < n