proposition: Lemma tuto_rot_addn : forall m n s, m + n <= size s -> rot (m + n) s = rot m (rot n s).
proof: Proof. move=> m n s; rewrite leq_eqVlt. case/predU1P=> [Emn|Hmn]. rewrite Emn rot_size. Search _ (rot _ (rot _ _) = _). rewrite rot_add_mod -Emn ?leq_addr ?leq_addl //. by rewrite Emn leqnn rot_size. rewrite -{1}(cat_take_drop n s) /rot !take_cat !drop_cat. Search _ (size (take _ _) = _). have Hns : n <= size s by apply: leq_trans (leq_addl _ _) (ltnW Hmn). rewrite !(size_takel Hns). have -> : m + n < n = false by rewrite ltnNge leq_addl. rewrite size_drop. have -> : m < size s - n by rewrite ltnNge leq_subLR -ltnNge addnC. by rewrite addnK catA. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(path choice fintype tuple finset)