proposition: Lemma notin0_part sh : is_part sh -> 0 \notin sh.
proof: Proof. elim: sh => // s0 sh IHsh Hpart. rewrite inE negb_or eq_sym. have /= -> := part_head_non0 Hpart. by apply: IHsh; move: Hpart => /= /andP[]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype