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