proposition: Lemma tuple_index_count (T : eqType) (n : nat) (s : n.-tuple T) (p : {pred T}) : #|[set j : 'I_n | p (tnth s j)]| = count p s.
proof: Proof. wlog x0 : n s p / T. { case: n s p => [|n] s p W; last exact/W/(thead s). by rewrite tuple0; apply: eq_card0 => -[j]. } rewrite (count_nth x0) cardsE cardE -(size_map (@nat_of_ord n)). apply/perm_size/uniq_perm. - by rewrite map_inj_uniq ?enum_uniq //; apply: ord_inj. - by rewrite filter_uniq // iota_uniq. move => k. rewrite mem_filter mem_iota add0n leq0n /=. have def_n : n = size s by case: s => /= s => /eqP->. apply/mapP/andP => [[[j Hj] p_j] -> /=|[p_k lt_k_n]]. by rewrite mem_enum /= unfold_in /tnth /= (set_nth_default x0) -?def_n // in p_j *. rewrite -def_n in lt_k_n. exists (Ordinal lt_k_n) => //. by rewrite mem_enum unfold_in /tnth /= (set_nth_default x0) // -def_n. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph sgraph) GraphTheory(dom partition coloring) mathcomp(ssrint) mathcomp(all_algebra)