proposition: Lemma rotD m n s : m + n <= size s -> rot (m + n) s = rot m (rot n s).
proof: Proof. move=> sz_s; rewrite [LHS]/rot -[take _ s](cat_take_drop n). rewrite 5!(catA, =^~ rot_size_cat) !cat_take_drop. by rewrite size_drop !size_takel ?leq_addl ?addnK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)