proposition: Lemma minhE : minh = - Posz (\max_(i < (size w).+1) (count_mem }} (take i w) - count_mem {{ (take i w))).
proof: Proof. rewrite /minh /prefixes. by rewrite big_map -{1}[(size w).+1]subn0 -/(index_iota _ _) big_mkord. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree