proposition: Lemma rotate_nat_add_add base offset len n: 0 < len → rotate_nat_add base (offset + n) len = (rotate_nat_add base offset len + n) `mod` len.
proof: Proof. intros ?. unfold rotate_nat_add. rewrite !Z2Nat.inj_mod, !Z2Nat.inj_add, !Nat2Z.id by lia. by rewrite Nat.add_assoc, Nat.add_mod_idemp_l by lia. Qed.
imports: Coq(QArith Qcanon) stdpp(well_founded) stdpp(options)