proposition: Lemma minh_neg : minh < 0.
proof: Proof. rewrite oppr_lt0 gtz0_ge1 -lerN2 -Hbal1. rewrite -{2}(take_size w). exact: minhP. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree