proposition: Lemma head_rot s x0 n : n < size s -> head x0 (rot n s) = nth x0 s n.
proof: Proof. move=> n_lt_s; rewrite /rot -nth0 nth_cat size_drop subn_gt0 n_lt_s. by rewrite -{2}[s](cat_take_drop n) nth_cat size_take n_lt_s ltnn subnn. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect)