proposition: Lemma flatten_equiv_cut_k s ss : s == flatten ss <-> ss \in cut_k (size ss) s.
proof: Proof. Proof using. split; first by move=> /eqP ->; apply (cut_k_flatten ss). move => /mapP[sh]; rewrite vect_n_kP => /andP[/eqP Hsum _] H; subst ss. by rewrite reshapeKr; last rewrite Hsum. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype seq) tools