proposition: Lemma vect_n_kP n k s : s \in vect_n_k n k = (sumn s == n) && (size s == k).
proof: Proof. apply/idP/idP; first exact: in_vect_n_k. by move=> /andP[]; apply: vect_n_k_in. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype seq) tools