proposition: Lemma cut_k_flatten ss : ss \in cut_k (size ss) (flatten ss).
proof: Proof. Proof using. rewrite /cut_k; apply/mapP. exists (shape ss); first exact (mem_shape_vect_n_k ss). by rewrite flattenK. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype seq) tools