proposition: Lemma intpartn0 : all_equal_to (rowpartn 0).
proof: Proof. by move=> sh /=; apply val_inj; rewrite /= val_intpartn0 rowpartnE. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype