proposition: Lemma part_head_non0 sh : is_part sh -> head 1 sh != 0.
proof: Proof. elim: sh => //= sh0 sh IHsh /andP[Head]. move/IHsh; apply: contraLR; rewrite !negbK => /eqP Hsh0. by move: Head; rewrite Hsh0 leqn0. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype