proposition: Lemma part_leq_head sh i : is_part sh -> i \in sh -> i <= head 0 sh.
proof: Proof. elim: sh => // sh0 sh IHsh Hpart. rewrite inE => /orP[/eqP->/= |]. by case: sh0 {Hpart} (part_head_non0 Hpart) => [|n _]//=. move: Hpart => /= => /andP[Hhead {}/IHsh /[apply]] /leq_trans; apply. by case: sh Hhead. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype