proposition: Lemma part0 sh : is_part sh -> sumn sh = 0 -> sh = [::].
proof: Proof. by move/part_head_non0; case: sh => //= [] [|s0]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype