proposition: Lemma evalseq_countE : evalseq_count =1 evalseq.
proof: Proof. elim => // l0 s /= <-; apply: (@eq_from_nth _ 0). rewrite size_incr_nth !size_map !size_iota /= {1}maxnC {1}/maxn. by case (ltngtP l0.+1 (foldr _ _ _)). move=> i; rewrite nth_incr_nth size_map => Hsz. rewrite (nth_map 0 _ _ Hsz); rewrite size_iota in Hsz. rewrite (nth_iota _ _ Hsz) add0n. case (ltnP i (foldr maxn 0 [seq i.+1 | i <- s])) => Hi. - rewrite (nth_map 0 _ _); last by rewrite size_iota. by rewrite (nth_iota _ _ Hi) /= add0n. - rewrite (nth_default 0) /=; last by rewrite size_map size_iota. congr (_ + _). elim: s Hi {Hsz} => // s0 s /=. move: (foldr _ _ _) => m IHs; rewrite /maxn. case (ltnP s0.+1 m) => Hs Hi. + by rewrite (IHs Hi) (ltn_eqF (leq_ltn_trans (leqnSn s0) (leq_trans Hs Hi))). + by rewrite (IHs (leq_trans Hs Hi)) (ltn_eqF Hi). Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass partition