proposition: Lemma rot_minn n s : rot n s = rot (minn n (size s)) s.
proof: Proof. by case: (leqP n (size s)) => // /leqW ?; rewrite rot_size rot_oversize. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)