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 proof rotate_nat_add_add_mod agnostic of the particular design decision.