proposition: Fact rowpartn_subproof d : is_part_of_n d (if d is 0 then [::] else [:: d]).
proof: Proof. by case: d => //= d; rewrite /is_part_of_n /= addn0 eq_refl. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype