proposition: Lemma nth_evalseq s i : nth 0 (evalseq s) i = count_mem i s.
proof: Proof. rewrite -evalseq_countE /evalseq_count. case: (ltnP i (foldr maxn 0 [seq i.+1 | i <- s])) => Hi. - by rewrite (nth_map 0) ?size_iota // nth_iota. - rewrite nth_default; last by rewrite size_map size_iota. elim: s Hi => // s0 s IHs /=. by rewrite geq_max => /andP[/ltn_eqF -> /= /IHs <-]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass partition