proposition: Lemma empty_intpartP (p : intpart) : sumn p = 0 -> p = empty_intpart.
proof: Proof. by move=> Hsum; apply val_inj => /=; apply: part0. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype