proposition: Fact colpartn_subproof d : is_part_of_n d (nseq d 1%N).
proof: Proof. elim: d => //= d /andP[/eqP -> ->]. rewrite add1n eq_refl andbT /=. by case: d. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype