proposition: Fact exists_minh : exists i : nat, height (take i w) == minh.
proof: Proof. rewrite /height minhE. have : (#|'I_(size w).+1| > 0)%N by rewrite card_ord. set F := BIG_F; move/(eq_bigmax_cond F) => [[i Hi _]]; rewrite {}/F /= => Hmax. case: (leqP (count_mem {{ (take i w)) (count_mem }} (take i w))) => [Hle |/ltnW]. - by exists i; rewrite -eqr_opp opprK opprB (subzn Hle) /= Hmax. - rewrite -subn_eq0 => /eqP Heq; move: Hmax; rewrite Heq => ->. by exists 0%N; rewrite take0. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree