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.

changed the description

Thanks for the MR!

@msammler Since you contributed this library, could you let us know what you think?

This MR looks fine to me. As far as I can see, I am not using rotate_nat_add_len_0 and rotate_nat_sub_len_0 in my development, and rotate_nat_add_len_0 was only used by rotate_nat_add_add_mod.

It's unfortunate that the stdlib does not have the following lemma:

Lemma Z_mod_nonneg x y : (0 ≤ y)%Z → (0 ≤ x `mod` y)%Z.
Proof.
  intros. assert (y = 0 ∨ 0 < y)%Z as [->|?] by lia.
  - by rewrite Zmod_0_r.
  - apply Z_mod_lt. lia.
Qed.

Then the proof in std++ would just be:

Lemma rotate_nat_add_add_mod base offset len:
  rotate_nat_add base offset len =
  rotate_nat_add (Z.to_nat (base `mod` len)%Z) offset len.
Proof.
  unfold rotate_nat_add.
  by rewrite Z2Nat.id, Zplus_mod_idemp_l by auto using Z_mod_nonneg with lia.
Qed.

It's unfortunate that the stdlib does not have the following lemma: Z_mod_nonneg

Indeed, Z_mod_nonneg_nonneg will be part of a lia/nia update: https://github.com/coq/coq/pull/14037

Excellent.

merged

mentioned in commit 0ce29e73