proposition: Lemma count_nth (T : Type) (x0 : T) (p : {pred T}) (s : seq T) : count p s = size [seq i <- iota 0 (size s) | p (nth x0 s i)].
proof: Proof. elim: s => //= a s ->; rewrite -[1]addn0 iotaDl filter_map fun_if /=. by rewrite size_map; case: (p a). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph sgraph) GraphTheory(dom partition coloring) mathcomp(ssrint) mathcomp(all_algebra)