proposition: Lemma rotK : cancel (rot n0) (rotr n0).
proof: Proof. move=> s; rewrite /rotr size_rot -size_drop {2}/rot. by rewrite rot_size_cat cat_take_drop. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)