proposition: Lemma rotate_nat_add_S base offset len: 0 < len → rotate_nat_add base (S offset) len = S (rotate_nat_add base offset len) `mod` len.
proof: Proof. intros ?. by rewrite <-Nat.add_1_r, rotate_nat_add_add, Nat.add_1_r. Qed.
imports: Coq(QArith Qcanon) stdpp(well_founded) stdpp(options)