proposition: Lemma in_vect_n_k n k s : s \in vect_n_k n k -> (sumn s == n) && (size s == k).
proof: Proof. elim: k n s => [| k IHk n]; first by case => [[| s0 s]|]. case => [|s0 s] /flattenP /= [ll /mapP[i Hi ->] /mapP[s' //]]. rewrite -/vect_n_k => /IHk /andP[/eqP Hsum /eqP Hsize] [-> ->]. rewrite Hsize /= eq_refl andbT Hsum. move: Hi; rewrite mem_iota add0n ltnS => /andP[_ Hi]. by rewrite addnC subnK. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype seq) tools