proposition: Lemma card_preim_nth (m : nat) (T : eqType) (s : seq T) (P : pred T) (u : T): size s = m -> #|[set i : 'I_m | preim (nth u s) P i]| = count P s.
proof: Proof. move=> Hsz. rewrite cardsE cardE /enum_mem -enumT /=. rewrite (eq_filter (a2 := (fun i : 'I_m => preim (nth u s) P i))); first last. by move=> i; rewrite inE unfold_in. rewrite -(size_map nat_of_ord) -filter_map val_enum_ord. have:= mkseq_nth u s; rewrite /mkseq. move=> /(congr1 (filter P))/(congr1 size). by rewrite [X in _ = X]size_filter filter_map size_map Hsz. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree