simplify internal helpers for divNatNZ and modNatNZ

[rgrover]

minor code cleanup for internal helpers of div and mod for Nats

[gallais]

Idris will not be able to see these refactored versions as obviously total. We have not yet turned the totality checker on for these libs but I am guessing that it will happen at some point.

[rgrover]

I can confirm that this implementation fails to satisfy the totality checker. This is surprising because mod' reduces its arguments at each recursive step.

If possible, I would like to understand why Idris cannot determine the totality of the more straightforward implementation. From my point of view, I have only removed some unnecessary bits of logic; the crux of the algorithm remains the same.

In any case, this pull request is of minor importance. The previous code was difficult to follow but was otherwise correct. I will withdraw this pull request for the sake of totality.

[gallais]

If possible, I would like to understand why Idris cannot determine the totality

The fact that minus left right is strictly smaller than left relies on a lot of implicit knowledge (right is non-zero because it's been checked before calling mod', left is non-zero because otherwise it would be true that lt left right for a non-zero right, and finally minus is size decreasing in its first argument when both of its arguments are non-zero).

Compare that to the obvious fact that left is smaller than S left used by the previous definition.

[rgrover]

Thanks :+1: