proposition: Lemma rotate_take_add l b i : i < length l → rotate_take b (rotate_nat_add b i (length l)) l = take i (rotate b l).
proof: Proof. intros ?. unfold rotate_take. by rewrite rotate_nat_sub_add. Qed.
imports: stdpp(options)