proposition: Lemma count_mem_vect_n_k_eq_1 n k s : s \in vect_n_k n k -> count_mem s (vect_n_k n k) = 1.
proof: Proof. elim: k n s=> [/= | k IHk n s]. by case=> s //=; rewrite mem_seq1 => /eqP ->. rewrite count_flatten -/vect_n_k -map_comp. case: s => [|s0 s]; first by rewrite vect_n_kP /= => /andP[_]. move/flatten_mapP; rewrite -/vect_n_k => [] [i]. rewrite mem_iota [iota _ _]lock add0n => Hs0. move/mapP => [t Ht [H1 H2]]; subst i; subst t. rewrite (eq_map (g := (fun i : nat => i == s0 : nat))). by unlock; rewrite sumn_pred1_iota add0n Hs0. move=> i; rewrite /= count_map /=. rewrite (eq_count (a2 := fun t => (i == s0) && (s == t))); first last. rewrite /= /preim => t /=. by apply/eqP/andP => [[-> ->] | [/eqP -> /eqP ->]]. case H : (i == s0) => /=; last by rewrite count_pred0. rewrite (eq_count (a2 := (xpred1 s))); last exact: eq_sym. by apply: IHk; rewrite (eqP H). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype seq) tools