Future proof rotate_nat_add_add_mod
This prepares rotate_nat_add_add_mod
for https://github.com/coq/coq/pull/14086 in a backwards compatible manner. Crucially, the design decision n mod 0 = 0
could change to n mod 0 = n
in future. This merge request makes rotate_nat_add_add_mod
agnostic of the particular design decision.
Edited by Andrej Dudenhefner