proposition: Lemma vect_n_k_in n k s : sumn s == n -> size s == k -> s \in vect_n_k n k.
proof: Proof. elim: k n s => [| k IHk n]. - by case => [s _ /nilP -> // | n]; case. - case => [// | s0 s] /eqP Hsum Hsize. apply/flattenP; rewrite -/vect_n_k /mkseq. exists (map (cons s0) (vect_n_k (n - s0) k)). + apply/mapP; exists s0; last by []. by rewrite mem_iota leq0n add0n /= ltnS -Hsum /=; apply: leq_addr. + apply/mapP; exists s; last by []. apply: IHk; first by rewrite -Hsum /= -{2}[s0]addn0 subnDl subn0. by move: Hsize. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype seq) tools