proposition: Lemma pfminh_size : (pfminh <= size w)%N.
proof: Proof. rewrite /pfminh; case: ex_minnP => pfmd /eqP Hpfmd pfmd_min. rewrite leqNgt; apply/negP => Habs. move: Hpfmd; rewrite (take_oversize (ltnW Habs)) -(take_size w). move=> /eqP/pfmd_min/leq_ltn_trans/(_ Habs). by rewrite ltnn. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree