proposition: Lemma mem_shape_vect_n_k ss : (shape ss) \in vect_n_k (size (flatten ss)) (size ss).
proof: Proof. Proof using. apply: vect_n_k_in; first by rewrite size_flatten. by rewrite size_map. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype seq) tools