proposition: Lemma rotate_nat_add_add_mod base offset len: rotate_nat_add base offset len = rotate_nat_add (base `mod` len) offset len.
proof: Proof. unfold rotate_nat_add. by rewrite Nat2Z.inj_mod, Zplus_mod_idemp_l. Qed.
imports: Coq(QArith Qcanon) stdpp(well_founded) stdpp(options)