proposition: Lemma rot_add_mod m n s : n <= size s -> m <= size s -> rot m (rot n s) = rot (if m + n <= size s then m + n else m + n - size s) s.
proof: Proof. move=> Hn Hm; case: leqP => [/rotD // | /ltnW Hmn]; symmetry. by rewrite -{2}(rotK n s) /rotr -rotD size_rot addnBA ?subnK ?addnK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)