proposition: Lemma subseq_rot p s n : subseq p s -> exists2 k, k <= n & subseq (rot k p) (rot n s).
proof: Proof. move=> /subseqP[m size_m ->]. exists (count id (take n m)); last by rewrite -mask_rot // mask_subseq. by rewrite (leq_trans (count_size _ _))// size_take_min geq_minl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)